Hi James,
Spec is defined as Init /\ [] [Next]_<<val,rdy,ack>>, but you seem to be
reading it as [] [Init /\ Next]_<<val,rdy,ack>> - in words you mix up
"Init holds at the beginning of the behavior _and_ Next holds in all
states of the behavior" with "Init and Next hold in all states of the
behavior".
If you replace conjunction in Spec with a disjunction, it would be ok if
your system just starts out with the initial configuration and continues
arbitrarily (remember, A \/ B is already true if A is true, regardless
of the truth of B).
cheers, Martin
> <mailto:tlaplus+unsubscribe@
On 01/31/2017 11:08 PM, James Mitchell wrote:
> 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
> ============================================================ =================
>
> --
> 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+unsubscribe@googlegroups.com
googlegroups.com >.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
> <mailto:tlaplus@googlegroups.com >.
> Visit this group at https://groups.google.com/group/tlaplus .
> For more options, visit https://groups.google.com/d/optout .
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/Tu-eVPAqF5E/ .unsubscribe
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com .
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 .