Re: [tlaplus] How to read the graph generated by TLC? Is there a way to specify its location?

[Michael Leuschel <leus...@xxxxxxxxxxxxxxxxxxxxx>]

I made a mistake while posting the clock example and accidentally replaced the Clock => []Init  theorem.

Below is the corrected model in case you want to try it out (and correct the bug ;-)).

---------------------- MODULE clock_init0 ----------------------

EXTENDS Naturals

VARIABLES

  hours,

  minutes,

  seconds

Init  ==    hours = 0

               /\ minutes = 0

               /\ seconds = 0 

Next  ==    hours' = (IF minutes # 59 THEN hours ELSE (hours + 1) % 12)

               /\ minutes' = (IF seconds # 59 THEN minutes ELSE (minutes + 1) % 60)

               /\ seconds' = (seconds + 1) % 60

Clock  ==  Init /\ [][Next]_<<hours, minutes, seconds>>

--------------------------------------------------------------

THEOREM  Clock => []Init

==============================================================