Specify and Verifying temporal properties in TLA+ Toolbox

46 views
Skip to first unread message

jevitha kp

unread,
Aug 15, 2017, 9:01:54 AM8/15/17
to tlaplus
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

Stephan Merz

unread,
Aug 15, 2017, 11:01:19 AM8/15/17
to tla...@googlegroups.com
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


--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

Reply all
Reply to author
Forward
0 new messages