// Test queueing of modelling-event triggered output events
// (Well-formedness: modelling event may trigger at most one output event)
interface ICallEmitMulti
{
  enum EmitResult {One, Two};
  in void req();
  in EmitResult reqValued();
  in void ack();
  in void done();
  out void ntfA();
  out void ntfB();
  behaviour
  {
    subint Counter {0..2};
    bool isWaiting = false;
    Counter pending = 0;
    {
      [otherwise]
      {
        on req: 
          {
            ntfA;
            ntfB;
            pending = 2;
            isWaiting = true;
          }
        on reqValued: 
          {
            ntfA;
            ntfB;
            pending = 2;
            isWaiting = true;
            reply(EmitResult.Two);
          }
        on ack, done: illegal;
      }
      [isWaiting]
      {
        on req, reqValued: illegal;
        on ack:
          {
            // Eplicit modelling of range check for 'pending' should not be necessary!
            // Currently required to prevent CSP compilation error due to otherwise 
            // unconstrained pending-- operation.
            [pending == 0]
              illegal;
            [otherwise]
              pending = pending - 1;
          }
        on done: 
          {
            [pending == 0] isWaiting = false;
            [otherwise] illegal;
          }
      }
    }
  }
}

interface ICallTrigger
{
  in void start();
  out void notLiveLock();
  behaviour
  {
    on start: 
      {
      }
  }
}

component QTriggerModeling
{
  provides ICallTrigger ict;
  requires ICallEmitMulti src;
  behaviour
  {
    bool behave = true;
    bool useVoid = true;
    {
      [behave]
      {
        [useVoid]
        {
          on ict.start(): 
            {
              src.req();
            }
          on src.ntfA(): 
            {
              src.ack();
            } // Allowed! ntfA + ntfB post is atomic action
          on src.ntfB(): 
            {
              src.ack();
              src.done();
              useVoid = false;
            }
        }
        [otherwise]
        {
          on ict.start(): 
            {
              ICallEmitMulti.EmitResult ignored = src.reqValued();
            }
          on src.ntfA(): 
            {
              src.ack();
            } // Allowed! ntfA + ntfB post is atomic action
          on src.ntfB(): 
            {
              src.ack();
              src.done();
              behave = false;
            }
        }
      }
      [otherwise] // misbehave
      {
        on ict.start(): 
          {
            src.req();
          }
        on src.ntfA(): 
          {
            src.ack();
            src.done();
          } // Illegal:  ntfA + ntfB post is atomic action => done after ntfB ack.
        on src.ntfB(): 
          {
            src.ack();
          }
      }
    }
  }
}