// Test queueing of modelling-event triggered output events
// (Well-formedness: modelling event may trigger at most one output event)

interface ITauEmitMulti
{
  in void ack();
  in void done();
  out void ntfA();
  out void ntfB();

  behaviour
  {
    bool isWaiting = false;
    bool isEmitting = false;

    {
      [otherwise]
      {
        on ack: {}
        on inevitable: 
          { 
            [!isEmitting] {ntfA; isEmitting = true;}
            [otherwise] {ntfB; isWaiting = true; isEmitting = false;}
          }
        on done: illegal;
      }
      [isWaiting]
      {
        on ack: {}
        on done: { isWaiting = false; }
      }
    }
  }
}

interface IDummy
{
  enum ReplyValue {Ok};
  in ReplyValue dummy();
  out void liveLockPreventer();

  behaviour
  {
    on dummy: {reply(ReplyValue.Ok);}
  }
}

component ConsumeMultiple
{
  provides IDummy d;
  requires ITauEmitMulti src;

  behaviour
  {
    bool behave = true;

    {
      [behave]
      {
        on d.dummy(): {reply(IDummy.ReplyValue.Ok);}
        on src.ntfA(): {src.ack();} // Allowed! ntfA + ntfB post is atomic action
        on src.ntfB(): {src.done(); behave = false;}
      }
      [otherwise] // misbehave
      {
        on d.dummy(): {reply(IDummy.ReplyValue.Ok);}
        on src.ntfA(): {src.done();} // Illegal: interface not isWaiting
        on src.ntfB(): {src.ack();}
      }
    }
  }
}