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; }
    }
  }
}

component async_context3 {
  provides IAsync p;
  behaviour {
    enum State { S0, S1, S2 };
    requires dzn.async i;
    requires dzn.async ii;

    State s = State.S0;

    [s.S0] {
      on p.e(): { i.req(); ii.req(); s = State.S1; }
      on p.c(): i.clr();
    }
    [s.S1] {
      on p.c(): { i.clr(); ii.clr(); s = State.S0; }
      on i.ack(): { s = State.S2; p.cb(); }
    }
    [s.S2] {
      on p.e(): illegal; // this illegal should lead to an compliance error
      on p.c(): {}
      on ii.ack(): s = State.S0;
    }
  }
}