[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Specify and Verifying temporal properties in TLA+ Toolbox



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


On 15 Aug 2017, at 15:01, jevitha kp <jev...@xxxxxxxxx> wrote:

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.