Hi
Specifying the Alternating bit protocol as component processes in PlusCal and showing it is a refinement of a one place buffer. The refinement works fo safety properties but fails when i try to check the liveness properties. I have attached a png showing a small fragment of the State Graph and the error trace. What I do not understand is why this is failing. The error trace is the cycle of three states in the top right of the State Graph but two of these states offer the ability to exit the loop (via an ssd step) but the translated PlusCal has added the strong fairness clauses for all the steps:
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
/\ SF_vars(ssd)
/\ SF_vars(sData)
/\ SF_vars(rData)
/\ SF_vars(wire)
/\ SF_vars(ackWire)
/\ SF_vars(sender)
I assume that I have misunderstood some thing but I thought that looping forever was prohibited by these strong fairness clauses. Hence I can not see how to correct my spec.
thanks in advance for any help david
