| Rev | Line | |
|---|
| [11] | 1 | #FAIL: fails even when weakened to AG(lamp=unlit -> EX(lamp=lit)) |
|---|
| 2 | # or to AG(lamp=lit -> EX(lamp=unlit)) |
|---|
| 3 | AG(((lamp = lit)->EX(lamp=unlit))*((lamp=unlit)->EX(lamp=lit))); |
|---|
| 4 | #PASS: passes even when strengthened to EF(int.state=go3) |
|---|
| 5 | # or to EF(int.state=go4). |
|---|
| 6 | EF((int.state=go3)+(int.state=go4)); |
|---|
| 7 | #PASS: no vacuous passes |
|---|
| 8 | EF EG((int.state=go3)+(int.state=go4)); |
|---|
| 9 | #FAIL: no vacuous failures |
|---|
| 10 | !EF EG((int.state=go3)+(int.state=go4)); |
|---|
| 11 | #FAIL: no vacuous failures |
|---|
| 12 | AG AF(!(int.state=go3)*!(int.state=go4)); |
|---|
| 13 | #FAIL: no vacuous failures |
|---|
| 14 | AG((interpretation = go) -> (train = absent)); |
|---|
| 15 | #PASS: passes even when strengthened to AG !(train = present2) |
|---|
| 16 | AG((interpretation = go) -> !(train = present2)); |
|---|
Note: See
TracBrowser
for help on using the repository browser.