[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Specify and Verifying temporal properties in TLA+ Toolbox
I'm trying to verify a temporal property that F ~> G, which is supposed to yield false in the specification given below, but the model checking reports no errors. Kindly guide on how to specify and verify temporal properties using TLA plus toolbox.
Init == hr = 1
Next == hr' = IF hr < 12 THEN hr + 1 ELSE 1
F == hr = 1
G == hr = 13
Spec == Init /\  [Next]_hr /\ (F ~> G)