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
oneMore:+
either
upx:+
x := x + 1;
or
upy:+
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.