Hi y'all,
Sorry if this's too basic for this list...
I'm trying to figure out how to use TLA+ Tools so I can learn TLA+, and so I downloaded it and typed in the AsynchInterface spec from page 27 of "Specifying Systems". Eventually I figured out that I needed to input "Spec" in the model's temporal formula, and I arbitrarily set "Data <- {12}" in the "What is the Model?" section (apparently, only specs that have been fully parameterized can be checked?). Neither of these cured the runtime Exceptions that were alluded to (but not displayed anywhere), so eventually I rechecked my model and found out that instead of having a conjunction in Spec, I had typed a disjunction instead.
This makes my brain hurt... Spec seems to say to me that Init remains true over time even though state transitions from Next are clearly violating Init's assumptions. Would someone mind opining on how I interpret the meaning of Spec?
Thanks,
James
P.S. How does TLA+ Tools handle the THEOREM bit? Is it ignored, or...?
P.P.S (The formatting of the cited model looks off in this editor, but all the "bullet /\" items are correctly indented in the editor.)
P.P.P.S. This's really neat... if I can figure out how to use it. :)
--------------------------------- MODULE a ---------------------------------
EXTENDS Naturals
CONSTANT Data
VARIABLES val, rdy, ack
TypeInvariant == /\ val \in Data
/\ rdy \in {0,1}
/\ ack \in {0,1}
---------------------------------------------------------------------------
Init == /\ val \in Data
/\ rdy \in {0,1}
/\ ack = rdy
Send == /\ rdy = ack
/\ val' \in Data
/\ rdy' = 1 - rdy
/\ UNCHANGED ack
Recv == /\ rdy /= ack
/\ ack' = 1 - ack
/\ UNCHANGED << val, rdy >>
Next == Send \/ Recv
Spec == Init /\ [][Next]_<<val, rdy,ack>>
-----------------------------------------------------------------------------
THEOREM Spec => []TypeInvariant
=============================================================================