source: vis_dev/vis-2.1/examples/treearbiter/8-arbit.ctl @ 12

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

Add vis
File size: 430 bytes
RevLine 
[11]1# never have both cells holding the token at the same time
2AG ( ! ( ( G1.C1.holdToken = myTRUE ) * ( G1.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 ( ! ( ( G1.P3.procState = lock ) * ( G1.P2.procState = lock) ) );
7
8# ensures liveness - needs fairness on the procs to pass
9AG ( ( G1.P3.procState = request ) -> AF ( G1.P3.procState = lock) );
Note: See TracBrowser for help on using the repository browser.