# MC: formula failed --- AF(FALSE)
# LE: language is not empty
# MC: formula passed --- AG(TRUE)
# MC: formula failed --- AG((ph0.state=HUNGRY -> AF(ph0.state=EATING)))
# INV: formula passed --- (((((ph0.state=READING + ph1.state=READING) + ph2.state=READING) * !((ph0.state=READING * ph1.state=READING))) * !((ph1.state=READING * ph2.state=READING))) * !((ph0.state=READING * ph2.state=READING)))
# LE: language is not empty
# MC: formula passed --- AG((ph0.state=HUNGRY -> AF(ph0.state=EATING)))
# LTL_MC: formula passed
# INV: formula passed --- (((((ph0.state=READING + ph1.state=READING) + ph2.state=READING) * !((ph0.state=READING * ph1.state=READING))) * !((ph1.state=READING * ph2.state=READING))) * !((ph0.state=READING * ph2.state=READING)))
# INV: formula passed --- (((((ph0.state=READING + ph1.state=READING) + ph2.state=READING) * !((ph0.state=READING * ph1.state=READING))) * !((ph1.state=READING * ph2.state=READING))) * !((ph0.state=READING * ph2.state=READING)))
# LE: language is not empty