| Hello Jevitha,
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.
Regards, Stephan
Hello,
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.
EXTENDS Naturals
VARIABLES hr
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)
Thanks, Jevitha
--
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.
|