// check whether silent transitions are considered when there is an outstanding req;
//   if correctly so, this model should report an illegal error.
interface IAsync {
  in void e();
  in void c();
  out void cb();

  behaviour {
    bool idle = true;
    [idle] {
      on e: idle = false;
      on c: {}
    }
    [!idle] {
      on e: illegal;
      on c: idle = true;
      on inevitable: { cb; idle = true; }
    }
  }
}

interface IAsync2 {
  enum Res { OK, NOK };

  in void e();
  in Res f();
  in void c();
  out void cb();

  behaviour {
    enum State { S0, S1, S2,S3 };
    State s = State.S0;
    [s.S0] {
      on e: s = State.S1;
      on c: {}
      on f: illegal;
    }
    [s.S1] {
      on e: illegal;
      on c: s = State.S0;
      on f: reply(Res.OK);
      on inevitable: { cb; s = State.S0; }
      on optional: s = State.S2;
    }
    [s.S2] {
      on e: illegal;
      on c: s = State.S0;
      on f: reply(Res.NOK);
      on inevitable: s = State.S3;
      on inevitable: { cb; s = State.S0; }
    }
    [s.S3] {
      on e: illegal;
      on c: s = State.S0;
      on f: reply(Res.OK);
      on inevitable: { cb; s = State.S0; }
    }
  }
}

component async_silent {
  provides IAsync p;
  requires IAsync2 r;
  behaviour {
    requires dzn.async i;
    bool idle = true;
    [idle] {
      on p.e(): { i.req(); r.e(); idle = false; }
      on p.c(): i.clr();
    }
    [!idle] {
      on p.e: illegal;
      on p.c(): { i.clr(); r.c(); idle = true; }
      on i.ack(): { 
	IAsync2.Res res = r.f();
        if (res == IAsync2.Res.NOK) 
          illegal; // the model checker should report this illegal;
      } 
      on r.cb(): { p.cb(); idle = true; }
    }
  }
}