interface IA {
  in void doAB();
  in void doBA();

  out void done();

  behaviour {
    bool idle = true;
 
    [idle] {
      on doAB: idle = false;
      on doBA: idle = false;
    }
    [!idle] {
      on doAB, doBA: illegal;
      on inevitable: { done; idle = true; }
    }
  }
}

interface IB {
  in void req();

  out void ack();

  behaviour {
    bool idle = true;
 
    [idle] 
      on req: idle = false;
    [!idle] {
      on req: illegal;
      on inevitable: { ack; idle = true; }
    }
  }
}

component A {
  provides IA p;
  requires IB r;
  
  behaviour {
    enum State { S0, S1, S2, S3};

    requires dzn.async i;

    State s = State.S0;
    
    [s.S0] {
      on p.doAB(): {
        i.req(); r.req(); s = State.S1;
      }
      on p.doBA(): {
        r.req(); i.req(); s = State.S1;
      }
    }
    [s.S1] {
      on i.ack(): s = State.S2;
    }
    [s.S2] {
      on r.ack(): { p.done(); s = State.S0; }
    }
  }
}

component B {
  provides IB p;
  
  behaviour {
    enum State { S0, S1 };

    requires dzn.async i;

    State s = State.S0;
    
    [s.S0] {
      on p.req(): {
        i.req(); s = State.S1;
      }
    }
    [s.S1] {
      on i.ack(): {
        p.ack(); s = State.S0;
      }
    }
  }
}

component async_ranking {
  provides IA p;

  system {
    A a;
    B b;

    p <=> a.p;
    a.r <=> b.p;
  }
}