This protocol is a simpler variant of the one bit sliding window protocol or the alternating bit protocol.The idea is to send the value of x from the sender side to the receiver side. The model consists of three distributed actions. The action
update updates the value of x. The actionsend copies x to c. The latter models the data channel between the sender and receiver. The actionreceive coplies c to y which then completes a protocol cycle. The actions are synchronized by two booleans variables: senderReady and recReady. Roughly speaking, the sender is allowed to update x if senderReady holds, whereas recReady means the the receiver is ready to accept a new data package.The send and receive actions are modelled as atomic. To help us test some more technical aspects of xMECH we deliberately break the update part into two atomic actions. For the same reason we also deliberately add an action which will actually never be executed (unreachable).
Here is the PLGA model of the protocol:
{ [root] : do :: (* updating data --it modelled as non-atomic *) { (senderReady) -> x = x+1 ; [mid] : senderReady=F ; } :: (* sending data --it is modelled as atomic*) (recReady /\ ~senderReady) -> atomic {c = x ; recReady=F ; senderReady=T ; } :: (* receiveing data --it is modelled as atomic*) (~recReady) -> atomic {y = c ; recReady=T ;} :: else block od ; (* this statement will never be executed *) [unreachable] : y = y - 1 ; }The picture below, which shows a graph of the state transitions of the protocol, may give a better idea how the protocol works. We neglect the effect intermediate transitions within the update block to simplify the graph.
![]()
Note that the protocol is actually sequential in most situations. It is however not totally sequential since it is non-deterministic when senderReady and not recReady.