[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Understanding AsynchInterface

Dear Guilherme,

the formula

  Init /\ [][Next]_vars

is evaluated over behaviors, i.e., infinite sequences of states. It is true of a behavior of the first state of the behavior satisfies the predicate Init and if all transitions (pairs of successive states) that change vars satisfy predicate Next.

In particular, the predicate Init (and in particular the equation rdy = ack) is only expected to hold of the first state, whereas it may be false later on. This is in line with what is illustrated at the beginning of the chapter.

TLA+ does not have a notion of "valid" or "invalid" states: a state simply assigns values to variables. Informally, one can say that a "valid" state for a given specification is one that satisfies the type correctness predicate associated with the specification (note, however, that users are not required to write such a predicate). The type correctness predicate for the specification of this example appears on p.25, and it does not require rdy and ack to have the same values.

Hope this helps?


On 2 Nov 2016, at 20:59, Guilherme C <guilhe...@xxxxxxxxx> wrote:


I am learning TLA+ reading the Specifying Systems book. I am reading Chapter 3, which presents the AsynchInterface.

There, in Figure 3, we have:
Spec == Init /\ [][Next]<<val, rdy, ack>>

and Init is defined with rdy = ack, which means that the states where ack and rdy have different values, Spec is false. Is there any reason for that? I got confused because in the beginning of this chapter, there is a list of supposedly valid states where rdy and ack are different, i.e., after a send command and before its acknowledgement. Wouldn't this case be also a valid state?

What am I missing in this specification?

Thanks for any help.



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