Re: [tlaplus] Loop not terminating

On Tuesday, April 27, 2021 at 2:52:58 PM UTC+1 Stephan Merz wrote:

Your algorithm may fail to terminate due to stuttering: any TLA+ specification of the form

Init /\ [][Next]_vars

may take stuttering steps, even infinitely many. In order to rule out infinite stuttering, add a fairness assumption of the form

WF_vars(Next)

to the specification generated by the PlusCal translator. If you write "fair algorithm" instead of "algorithm", the PlusCal translator will generate that fairness condition for you.

Stephan

On 27 Apr 2021, at 15:45, c.burge...@gmail.com <c.burge...@xxxxxxxxx> wrote:

Hi again :)

I am trying out different implementations of a while loop, and I have this little pluscal algorithm:

-------------------------------- MODULE loop --------------------------------
EXTENDS Naturals, TLC
(*
--algorithm loop {
variables y;
{
A:
goto C;
B:
y:=y-1;
C:
if (y > 0){
goto B };
D: skip;
}
}
end algorithm;
*)

I give y an initial value of 10, but when I ask TLC to check for termination, it fails. Why would that be? The error trace shows the loop working as expected, with y decreasing from 10 to 0 in increments of 1.

--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6b4b773b-6c16-4f7b-a35d-6736d5c70db8n%40googlegroups.com.