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

Re: How does Fairness relate to the State Graph

I'm afraid I don't know PlusCal well, and I believe your issue has much to do with the precise semantics of PlusCal, but the following TLA+ works and verifies termination:

EXTENDS Naturals


ASSUME Size \in Nat


vars == << x, y >>

Init == /\ x = 0

        /\ y = 0


UpX == /\ x' = x + 1

       /\ UNCHANGED y


UpY == /\ y' = (y + 1 ) % Size

       /\ UNCHANGED x


Next == IF (x < Size)

           THEN UpX \/ UpY

           ELSE UNCHANGED vars \* prevent deadlock

Spec == Init /\ [][Next]_vars /\ WF_vars(UpX) /\ WF_vars(UpY) 

Termination == <>(x = Size)

Fairness has particular formal definition in TLA+, i.e. WF_x(A) is defined as a specific temporal formula specifying a liveness property.
I don't know if it would even be possible to define fairness in the way you suggest in a linear temporal logic, but Stephan will know more about this. Even if it could be defined in that way, it may be a bad idea: actions may well have an infinite number of possible next states, and specifying any such action as fair would automatically make your formula false and your specification empty. On the other hand, there is always just a finite number of formulas in a specification, so there are simple syntactic rules that determine when a fairness property is realizable.


On Wednesday, February 6, 2019 at 10:21:22 PM UTC+1, david streader wrote:
Thanks Ron
      so  fairness (if offered infinitely often must eventually be taken) in TLA+ is only between differently named steps and, as I said, it is the fact that the State Graph has both looping and exiting steps with the same name  that means that never taking the infinitely offered exit  is deemed fair. Remember it is a design decision how to check fairness.  As the state graph is build from the TLA+ fairness could be checked in the way I thought it would have been.

 Thats good to know that I need better use of labels  but I have added labels on every line I am allowed to and still  can not get termination with the current definition of fairness.

begin Count:

  while (x<Size) do




    x := x + 1;



    y := (y + 1)%Size;

  end either;

I know that the tool tells me that even restricting ourselves to  fair behavior it is possible for this algorithm to never terminate. But this is not fair behavior as I understand it to be unless I conclude that the Calplus either.. or .. construct is inherently unfair? I interpret fairness to require that upx:+ must be taken more that Size times in any fair execution.