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;