Re: [tlaplus] specifying systems book, Figure 3.1 -- bug? -- seems impossible to receive in AsyncInterface

[Stephan Merz <stepha...@xxxxxxxxx>]

I don't understand your argument. 

As you have observed, the Rcv action is not enabled in the initial state because ack = rdy. But the Send action is enabled, and it will flip the rdy bit. This will in turn enable the Rcv action (and in fact disable Send).

This disproves your claim that the receive action can never occur. In fact, the specification forces Send and Rcv to alternate (with stuttering transitions occurring in between). The specification does not assert that the Init always holds: formula Spec asserts that Init holds initially and that every non-stuttering transition satisfies Next. Perhaps you have been confused by the meaning of the "always" operator of temporal logic?

Regards,
Stephan


> On 06 Jun 2016, at 04:45, j.e....@xxxxxxxxx wrote:
> 
> 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.
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.