specifying systems book, Figure 3.1 -- bug? -- seems impossible to receive in AsyncInterface

[j.e....@xxxxxxxxx]

On page 27/Section 3.1 of

http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf

the book "Specifying Systems", there is a spec for AsynchInterface in Figure 3.1.

It seems to me that the interface contains an error because it can never Receive, due to the assertion that "ack = rdy" in the Init definition.  The definition of Rcv requires that rdy != ack. Since the Spec insists that Init always hold, it would be impossible to ever have Rcv hold, no?

To fix this, I suppose one could either remove the ack = rdy from the Init definition, or say Spec = Init \/ [Next]_<val,rdy,ack>  -- using an OR instead of an AND, but neither of these seems fully satisfactory, since they loosen the spec substantially.