Hi
I have encoded the Alternating Bit Protocol as several PlusCal processes in a style that hopefully would be familiar to anyone with a back ground in Process algebras. The specification is in the attached single Module abpPar.tla. It includes some fairness properties and has been shown to satisfy the liveness property Fin.
I decomposed the problem into separate processes that can be found in separate modules, abpSender.tla, abpReceiver.tla and abpWire.tla Then I wrote a module for a one place buffer, onePlaceBufferSpec.tla then showed that abpModular.tla satisfied the one place buffer. But only if neither included fairness properties. Although I was able to specify fairness on onePlaceBufferSpec.tla I can not see how to do this on abpModular.tla. Any offers of how to specify fairness on abpModular.tla would be greatly appreciated.
Also any comments on how the specifications might be improved while still having Sender Receiver and Channels in seperate process would also be very usful.
many thanks in advance previous discussions have been very helpful.
kind regards david