I'm looking at the Alternating Bit Protocol implementation" in Fig 14.1b of Specifying Systems and have a couple of questions:
- It seems to me that the msgQ does not grow in any useful way. By that I mean it can't be used for sending multiple messages, only for resending a message multiple times. Multiple messages cannot be sent because a message only gets sent if sAck = sBit, and this won't happen after a send until an Ack comes back from the receiver. Is that correct? If so, why maintain a queue at all?
- Instead of explicitly modeling the loss of messages and acks, would it have worked to simply OR in a disjunct that simply "loses" the data. That is RcvMsg would read (/\ msgQ # <<>> /\ msgQ'= Tail(msgQ) /\ rBit'=Head(msgQ)[1] /\ rcvd'=Head(msgQ)[2] /\ UNCHANGED<<ackQ; sBit; sAck; sent>>) \/ (/\ msgQ # <<>> /\ msgQ'= Tail(msgQ) /\ UNCHANGED <<ackQ; sBit; sAck; sent, sBit, rcvd>>)
Thanks