source:
vis_dev/vis-2.1/examples/arbiter/arbiter.ltl
@
11
Last change on this file since 11 was 11, checked in by , 13 years ago | |
---|---|
File size: 168 bytes |
Rev | Line | |
---|---|---|
[11] | 1 | # safety: mutual exclusion |
2 | G !(ackA=1 * ackB=1 + ackB=1 * ackC=1 + ackC=1 * ackA=1); | |
3 | ||
4 | # liveness: | |
5 | G(reqA=1 -> F ackA=1); | |
6 | G(reqB=1 -> F ackB=1); | |
7 | G(reqC=1 -> F ackC=1); |
Note: See TracBrowser
for help on using the repository browser.