[tlaplus] Loop not terminating

["c.burge...@xxxxxxxxx" <c.burge.glasgow@xxxxxxxxx>]

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