FSM depth =                 11
reachable states =      186876
# LE: language is not empty
# MC: formula failed --- AF(FALSE)
# LE: language emptiness check passes
# MC: formula passed --- AG(TRUE)
# MC: formula failed --- AG(((lamp=lit -> EX(lamp=unlit)) * (lamp=unlit -> EX(lamp=lit))))
# MC: formula passed --- EF((int.state=go3 + int.state=go4))
# MC: formula passed --- EF(EG((int.state=go3 + int.state=go4)))
# MC: formula failed --- !(EF(EG((int.state=go3 + int.state=go4))))
# MC: formula failed --- AG(AF((!(int.state=go3) * !(int.state=go4))))
# MC: formula failed --- AG((interpretation=go -> train=absent))
# MC: formula passed --- AG((interpretation=go -> !(train=present2)))
FSM depth =                 16
reachable states =      352544
# LTL_MC: formula failed
FSM depth =                 11
reachable states =      445404
# LTL_MC: formula failed
FSM depth =                 18
reachable states =      623201
# LTL_MC: formula failed
FSM depth =                 11
reachable states =      373752
# LTL_MC: formula passed
# MC: formula failed --- AG(((lamp=lit -> EX(lamp=unlit)) * (lamp=unlit -> EX(lamp=lit))))
# MC: Vacuous failure : lamp=lit
# MC: Vacuous failure : lamp=unlit
# MC: Vacuous failure : lamp=unlit
# MC: Vacuous failure : lamp=lit
# MC: formula passed --- EF((int.state=go3 + int.state=go4))
# MC: Vacuous pass : int.state=go3
# MC: Vacuous pass : int.state=go4
# MC: formula passed --- EF(EG((int.state=go3 + int.state=go4)))
# MC: No vacuous passes
# MC: formula failed --- !(EF(EG((int.state=go3 + int.state=go4))))
# MC: No vacuous failures
# MC: formula failed --- AG(AF((!(int.state=go3) * !(int.state=go4))))
# MC: No vacuous failures
# MC: formula failed --- AG((interpretation=go -> train=absent))
# MC: No vacuous failures
# MC: formula passed --- AG((interpretation=go -> !(train=present2)))
# MC: Vacuous pass : interpretation=go