[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.