parameter u1; parameter u2; P = (a -> Wait[u2]; b -> Stop) interrupt[u1] c -> P; #synthesize P with u1 = 1, u2 = 2; #synthesize P with u1 = 2, u2 = 1; #synthesize P reachesall; #assert P deadlockfree;