| 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? Stephan
|