FSM depth =                  2
reachable states =           5
# LE: language is not empty
# LE: language emptiness check passes
# LE: language is not empty
# MC: formula passed --- AG((ioh.state=PENDING -> AF(ioh.state=OKAY)))
# MC: formula passed --- AG((player_A.state=BALL + player_B.state=BALL))
# MC: formula passed --- AF((player_A.state=BALL ^ player_B.state=BALL))
# MC: formula passed --- AG((player_A.state=BALL + player_B.state=BALL))
# MC: formula failed --- AF((player_A.state=BALL ^ player_B.state=BALL))