# never have both cells holding the token at the same time
G !(G1.C1.holdToken = myTRUE * G1.C2.holdToken = myTRUE);

# never have G1.P3 and G1.P2 holding the token;
# actually need a formula for each pair of procs...
G !(G1.P3.procState = lock * G1.P2.procState = lock);

# ensures liveness - needs fairness on the procs to pass
G (G1.P3.procState = request -> F(G1.P3.procState = lock));