[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Q about the Alternating Bit Protocol example
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) /\ rcvd'=Head(msgQ) /\ UNCHANGED<<ackQ; sBit; sAck; sent>>) \/ (/\ msgQ # <<>> /\ msgQ'= Tail(msgQ) /\ UNCHANGED <<ackQ; sBit; sAck; sent, sBit, rcvd>>)
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9efaf26c-d79d-42af-a2c7-f8d60b980527%40googlegroups.com.