Hello,
Apologies for the rather broad question, but as a newcomer to formal methods, figure 3.2 (see attachement) has left me scratching my head.
This spec describes an asynchronous channel interface, which is particularly interesting to me as the engineering problem that led me to learn TLA+ involves asynchronous broadcast. As such, I'm trying to conceptually anchor my own problem to this very simple spec. What's "bothering" me is that this spec seems to define a system in which
- a channel is initially only able to send
- a channel is able to receive only after having sent
- a channel oscillates between an "able to send"-state and an "able to receive"-state, which precludes (e.g.) being able to receive twice in a row
I believe 1 to be true because Init states that chan.ack = chan.ready, which is a precondition for entering a Send state.
I believe 2 to be true because Send transitions to a state where ack != rdy and Rcv transitions to a state where ack = rdy.
I believe 3 to be true because, Rcv requires chan.rdy != chan.ack.
My questions are as follows:
- Is my reading of the spec correct, or have I missed something?
- Is this a toy example of an asynchronous send/recv interface that was simplified for pedagogical purposes, or is there some reason why such an interface must behave in this way?
Thank you very much in advance for your insight. In the meantime, thank you very much, Dr. Lamport, for your extremely helpful book and video series!
Regards,
