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

Understanding AsynchInterface


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.