- main("meet.fsm","mymeet.ctl");
Model checker
(EUtrue(ANDPspeakTgetFloor)) : false
(~(EUtrue(ANDPspeakTgetFloor))) : true
(~(EUtrue(~(ORPmoderatePhold)))) : true
(~(EUtrue(~(OR(~Phold)(AX(AUtrue(~Phold))))))) : false
(EUtrue(ANDTgrabFloorTdropFloor)) : false
(EUtrue(ANDTreleaseFloorTgetFloor)) : false
(EUtrue(ANDTaddpTdelp)) : true
Done evaluating.
val it = () : unit
-