interface IAsync {
  in void e();
  in void c();
  out void cb();
  out void ping();

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

interface IPing {
  in void dummy();
  out void ping();

  behaviour {
    on dummy: {}
    on optional: ping;
  }
}

component async_prio {
  provides IAsync p;
  requires IPing r;
  behaviour {
    requires dzn.async i;
    bool idle = true;
    [idle] {
      on p.e(): { i.req(); idle = false; }
      on p.c(): i.clr();
      on r.ping(): p.ping();
    }
    [!idle] {
      on p.e: illegal;
      on p.c(): { i.clr(); idle = true; }
      on i.ack(): { p.cb(); idle = true; }
      on r.ping: illegal;
    }
  }
}