source: vis_dev/vis-2.1/examples/treearbiter/4-arbit.ctl @ 14

Last change on this file since 14 was 11, checked in by cecile, 13 years ago

Add vis
File size: 412 bytes
RevLine 
[11]1# never have both cells holding the token at the same time
2AG ( ! ( ( C1.holdToken = myTRUE ) * ( C2.holdToken = myTRUE) ) );
3
4# never have G1.P3 and G1.P2 holding the token;
5# actually need a formula for each pair of procs...
6AG ( ! ( ( P3.procState = lock ) * ( P2.procState = lock) ) );
7
8# ensures liveness - needs fairness on the procs to pass
9AG ( ( P3.procState = request ) -> AF ( P3.procState = lock) );
Note: See TracBrowser for help on using the repository browser.