From my understanding (I'm also new), it works something like this: while it's true that the _expression_ Spec will be false after a send command, we're not using Spec as an _expression_. Instead, we're using it as a specification. If you put the specification in the TLA+ Toolbox and open the .cfg file it creates, you'll see something like this:
TLC (see chapter 14) handles specifications different than expressions. First it uses the state predicate to compute all possible initial states, then it uses the temporal bits to compute the possible transitions. So even though Init is false after the first transition, since we're not using Spec as an _expression_ it does not matter in this case.
You can make things more explicit by replacing the specification in the .cfg with
and not even need to define
Spec in the first place, but I don't think you can use this with fairness properties. Hope this makes sense!
Hillel
On Wednesday, 2 November 2016 14:59:42 UTC-5, Guilherme C wrote:
Hi,
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.
Best,
Guilherme