interface I { in void e(); in void a(); out void ec(); out void ac(); behaviour { enum State { idle, busy, aborting }; State s = State.idle; [s.idle] { on e: s = State.busy; on a: s = State.aborting; } [s.busy] { on e: illegal; on a: s = State.aborting; on inevitable: { ec; s = State.idle;} } [s.aborting] { on e: illegal; on a: illegal; on inevitable: { ac; s = State.idle;} } } } interface II { in void e(); in void a(); out void ec(); out void ac(); behaviour { enum State { idle }; State s = State.idle; [s.idle] { on e: ec; on a: ac; } } } component asyncsync { provides I p; requires external II r; behaviour { enum State { idle, busy, aborting }; State s = State.idle; [s.idle] { on p.e(): { r.e(); s = State.busy; } on p.a(): { r.a(); s = State.aborting;} on r.ec: illegal; on r.ac: illegal; } [s.busy] { on p.e: illegal; on p.a(): { r.a(); s = State.aborting;} on r.ec(): { p.ec(); s = State.idle;} on r.ac(): illegal; } [s.aborting] { on p.e: illegal; on p.a: illegal; on r.ec(): {} on r.ac(): { p.ac(); s = State.idle;} } } }