source: vis_dev/vis-2.1/examples/treearbiter/4-arbit.fair @ 16

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

!(P2.procState=lock);

!(P3.procState=lock);

!(P4.procState=lock);