Newbie Q -- "Spec" from the "AsynchInterface" example -- how to interpret?

38 views
Skip to first unread message

James Mitchell

unread,
Jan 31, 2017, 5:08:26 PM1/31/17
to tlaplus
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
=============================================================================

Leslie Lamport

unread,
Jan 31, 2017, 5:26:18 PM1/31/17
to tlaplus
Hi James,

To answer your first question, notice the [] (Box) in the formula Spec
and look up that symbol in the index of "Specifying Systems".

TLC ignores THEOREMs.  The TLAPS proof system allows you to prove
them, but you're probably not ready for that.

I suggest looking at the TLA+ Hyperbook to find out about using TLC.
(There's a link to it on the TLA+ Web page.)

Good luck,

Leslie

Martin

unread,
Feb 1, 2017, 5:34:19 AM2/1/17
to tla...@googlegroups.com
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
> --
> 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
> <mailto:tlaplus+u...@googlegroups.com>.
> To post to this group, send email to tla...@googlegroups.com
> <mailto:tla...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

James Mitchell

unread,
Feb 1, 2017, 10:31:31 AM2/1/17
to tla...@googlegroups.com
Thanks -- you're right.  Not knowing temporal logic, I was reading it as "Init is always true, along with each state transition selected from Next".

:)

James



> 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.

--
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...@googlegroups.com.
Reply all
Reply to author
Forward
0 new messages