[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] problems debugging liveness errors.

     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

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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

Attachment: abpLoop.png
Description: PNG image