interface IAsync {
  in void e();
  in void c();
  out void cb1();
  out void cb2();

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

subint int {0..2};
extern foo $int$;

component async_order {
  provides IAsync p;
  behaviour {
    requires dzn.async i1;
    requires dzn.async i2;
    int num = 0;
    [num==0] {
      on p.e(): { i1.req(); i2.req(); num = 2; }
      on p.c(): {}
    }
    [0<num] {
      on p.e: illegal;
      on p.c(): { i1.clr(); i2.clr(); num = 0; }
      on i1.ack(): { p.cb1(); num = num-1; }
      on i2.ack(): { p.cb2(); num = num-1; }
    }
  }
}

component cb1_cancel {
  provides IAsync p;
  requires IAsync r;
  behaviour {
    on r.cb1 (): r.c ();
    on r.cb2 (): p.cb2 ();
    on p.e (): r.e ();
    on p.c (): {}
  }
}