Loop not terminating

[c.burge...@gmail.com]

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.

[Stephan Merz]

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

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

[c.burge...@gmail.com]

Thanks, that's very helpful!

[c.burge...@gmail.com]

I see that I was not yet familiar with the concepts of stuttering and fairness, but a quick google has enlightened me :)