source:
vis_dev/vis-2.1/examples/treearbiter/8-arbit.ctl
@
11
Last change on this file since 11 was 11, checked in by , 13 years ago | |
---|---|
File size: 430 bytes |
Line | |
---|---|
1 | # never have both cells holding the token at the same time |
2 | AG ( ! ( ( 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... |
6 | AG ( ! ( ( G1.P3.procState = lock ) * ( G1.P2.procState = lock) ) ); |
7 | |
8 | # ensures liveness - needs fairness on the procs to pass |
9 | AG ( ( G1.P3.procState = request ) -> AF ( G1.P3.procState = lock) ); |
Note: See TracBrowser
for help on using the repository browser.