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