# P1 doesnt hold the token forever
!(P1.procState=lock);

!(P2.procState=lock);

!(P3.procState=lock);

!(P4.procState=lock);