source: vis_dev/vis-2.1/examples/dcnew/dcnew.ctl @ 14

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

Add vis

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