Line | |
---|
1 | # there is always at least one ball in play |
---|
2 | # (passes with or without fairness constraint) |
---|
3 | AG(!((ball_1.state=OUT_OF_PLAY) * (ball_2.state=OUT_OF_PLAY))); |
---|
4 | |
---|
5 | # if player_A produces IDLE now, then he will HIT sometime |
---|
6 | # in the future (only passes with fairness constraint) |
---|
7 | AG((player_A.out=IDLE) -> AF(player_A.out=HIT)); |
---|
8 | |
---|
9 | # Eventually only one ball is in play. Note ^ denotes XOR. |
---|
10 | # (should fail with or without fairness constraints) |
---|
11 | AF((ball_1.state=OUT_OF_PLAY) ^ (ball_2.state=OUT_OF_PLAY)); |
---|
12 | |
---|
13 | # There exists the possibility that eventually only one ball |
---|
14 | # is in play (should pass with or without fairness constraints) |
---|
15 | EF((ball_1.state=OUT_OF_PLAY) ^ (ball_2.state=OUT_OF_PLAY)); |
---|
16 | |
---|
17 | # there are always two balls in play |
---|
18 | # (fails with or without fairness constraint) |
---|
19 | AG(!(ball_1.state=OUT_OF_PLAY) * !(ball_2.state=OUT_OF_PLAY)); |
---|
20 | |
---|
21 | |
---|
Note: See
TracBrowser
for help on using the repository browser.