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

!(G1.P2.procState=lock);

!(G1.P3.procState=lock);

!(G1.P4.procState=lock);

!(G2.P1.procState=lock);

!(G2.P2.procState=lock);

!(G2.P3.procState=lock);

!(G2.P4.procState=lock);