Hi
I wrote a simple Process that my intuition tells me under a strong fairness assumption will terminate (included below). The State graph (attached) also informally confirms that under strong fairness the loops will all exit and the process will terminate.
TLC fails the Termination check. I am interested in what I can do to remedy this?
I tried editing /\ WF_vars(Next) to /\ SF_vars(Next) but to it did not change anything.
The Error Trace is simply two Count steps that form a loop. But with the specification /\ SF_vars(counter) I think this should not stop the Termination.
Hopefully I have missed something simple?
kind regards david
EXTENDS TLC, Integers
CONSTANT Size
(* --fair algorithm counter
variable x = 0, y = 0;
fair+ process counter = "counter"
begin Count:
while (x<Size) do
either
await (x<Size);
\* upx:+
x := x + 1;
or
\* upy:+
y := (y + 1)%Size;
end either;
end while;
end process;
end algorithm; *)
\* BEGIN TRANSLATION
VARIABLES x, y, pc
vars == << x, y, pc >>
ProcSet == {"counter"}
Init == (* Global variables *)
/\ x = 0
/\ y = 0
/\ pc = [self \in ProcSet |-> "Count"]
Count == /\ pc["counter"] = "Count"
/\ IF (x<Size)
THEN /\ \/ /\ (x<Size)
/\ x' = x + 1
/\ y' = y
\/ /\ y' = (y + 1)%Size
/\ x' = x
/\ pc' = [pc EXCEPT !["counter"] = "Count"]
ELSE /\ pc' = [pc EXCEPT !["counter"] = "Done"]
/\ UNCHANGED << x, y >>
counter == Count
Next == counter
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
/\ SF_vars(counter)
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION