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

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

On page 27/Section 3.1 of


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.