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 {
  in void e();
  in void c();
  out void cb1();
  out void cb2();

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

component async_synccb2 {
  provides IAsync p;
  requires IAsync2 r;
  behaviour {
    enum State {S0,S1,S2,S3};
    State s = State.S0;
    requires dzn.async i;

    on p.c(): { r.c(); i.clr(); s = State.S0; }
    
    [s.S0] {
      on p.e(): { r.e(); s = State.S1; }
    }
    [s.S1] {
      on r.cb1(): { i.req(); s = State.S2; }
    }
    [s.S2] {
      on r.cb2(): { s = State.S3; }
    }
    [s.S3] {
      on i.ack(): { p.cb(); s = State.S0; }
    }
  }
}