source: vis_dev/vis-2.1/examples/dcnew/check_result @ 11

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

Add vis
File size: 1.8 KB
Line 
1FSM depth =                 11
2reachable states =      186876
3# LE: language is not empty
4# MC: formula failed --- AF(FALSE)
5# LE: language emptiness check passes
6# MC: formula passed --- AG(TRUE)
7# MC: formula failed --- AG(((lamp=lit -> EX(lamp=unlit)) * (lamp=unlit -> EX(lamp=lit))))
8# MC: formula passed --- EF((int.state=go3 + int.state=go4))
9# MC: formula passed --- EF(EG((int.state=go3 + int.state=go4)))
10# MC: formula failed --- !(EF(EG((int.state=go3 + int.state=go4))))
11# MC: formula failed --- AG(AF((!(int.state=go3) * !(int.state=go4))))
12# MC: formula failed --- AG((interpretation=go -> train=absent))
13# MC: formula passed --- AG((interpretation=go -> !(train=present2)))
14FSM depth =                 16
15reachable states =      352544
16# LTL_MC: formula failed
17FSM depth =                 11
18reachable states =      445404
19# LTL_MC: formula failed
20FSM depth =                 18
21reachable states =      623201
22# LTL_MC: formula failed
23FSM depth =                 11
24reachable states =      373752
25# LTL_MC: formula passed
26# MC: formula failed --- AG(((lamp=lit -> EX(lamp=unlit)) * (lamp=unlit -> EX(lamp=lit))))
27# MC: Vacuous failure : lamp=lit
28# MC: Vacuous failure : lamp=unlit
29# MC: Vacuous failure : lamp=unlit
30# MC: Vacuous failure : lamp=lit
31# MC: formula passed --- EF((int.state=go3 + int.state=go4))
32# MC: Vacuous pass : int.state=go3
33# MC: Vacuous pass : int.state=go4
34# MC: formula passed --- EF(EG((int.state=go3 + int.state=go4)))
35# MC: No vacuous passes
36# MC: formula failed --- !(EF(EG((int.state=go3 + int.state=go4))))
37# MC: No vacuous failures
38# MC: formula failed --- AG(AF((!(int.state=go3) * !(int.state=go4))))
39# MC: No vacuous failures
40# MC: formula failed --- AG((interpretation=go -> train=absent))
41# MC: No vacuous failures
42# MC: formula passed --- AG((interpretation=go -> !(train=present2)))
43# MC: Vacuous pass : interpretation=go
Note: See TracBrowser for help on using the repository browser.