you need to indicate the specification that you want to verify as one TLA+ formula, and the property to be verified by another one. You appear to include the property F ~> G in the specification, hence the model checker will consider all executions that satisfy Spec. Since there are no such executions, Spec => Prop holds for whatever property Prop you may define.
Presumably you meant to define
Spec == Init /\ [Next]_hr /\ WF_hr(Next)
then enter F ~> G as the (temporal) formula to be verified by TLC.
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)
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
Visit this group at https://groups.google.com/group/tlaplus
For more options, visit https://groups.google.com/d/optout