1 | FSM depth = 11 |
---|
2 | reachable 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))) |
---|
14 | FSM depth = 16 |
---|
15 | reachable states = 352544 |
---|
16 | # LTL_MC: formula failed |
---|
17 | FSM depth = 11 |
---|
18 | reachable states = 445404 |
---|
19 | # LTL_MC: formula failed |
---|
20 | FSM depth = 18 |
---|
21 | reachable states = 623201 |
---|
22 | # LTL_MC: formula failed |
---|
23 | FSM depth = 11 |
---|
24 | reachable 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 |
---|