[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: When TLC error trace send with stuttering - what does this mean?

Many thanks   I never thought of stuttering as only occurring when a guard was satisfied that explains a lot.


If I seem to nitpicking it is just because  I am not finding debugging livenes easy. 

With spec 

EXTENDS  Naturals 


Init == x=0

Inc == x<5 /\ x'=x+1

Reset == x=5 /\ x'=0

Spec == Init /\ [][Inc \/ Reset]_x 

          (*   /\ SF_<<x>>(Inc) *)

             /\ SF_<<x>>(Reset)

where stuttering is reported  depends upon what property you ask as well as the spec itself.

with <> (x=2) it is after x = 1 but with  <> (x=4) its is after x = 3.

Consequently it was important that I stopped interpreting it to be an improvement that the spec was not  stuttering so soon. 

Does the addition of liveness conditions change the State Graph to indicate where infinite stuttering might occur?



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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.