Specify and Verifying temporal properties in TLA+ Toolbox

[jevitha kp <jev...@xxxxxxxxx>]

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