[11] | 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 |
---|