interface ihello
{
  in void hello();
  out void world();

  behaviour
  {
    bool pending = false;
    [!pending] on hello: pending = true;
    [pending] on hello: illegal;
    [pending] on inevitable: {pending = false; world;}
  }
}

component async_multiple_provides
{
  provides ihello l;
  provides ihello r;

  behaviour
  {
    requires dzn.async i;

    bool pending_left = false;
    bool pending_right = false;

    [!pending_left && !pending_right] {
      on l.hello(): {pending_left = !pending_left; i.req();}
      on r.hello(): {pending_right = !pending_right; i.req();}
    }
    [!pending_left && pending_right] {
      on l.hello(): pending_left = true;
      on i.ack(): {pending_right = false; r.world();}
    }
    [pending_left && !pending_right] {
      on r.hello(): pending_right = true;
      on i.ack(): {pending_left = false; l.world();}
    }
    [pending_left && pending_right] on i.ack(): {pending_left = false; i.req(); l.world();}
  }
}