Re: [tlaplus] Re: When TLC error trace send with stuttering

When TLC reports a counter-example to an invariant, it is guaranteed to be of smallest length because the state space is explored using breadth-first search [1]. Checking liveness properties relies on exploring strongly connected components of the state graph and the above guarantee does not hold. The state graph is still the same, independently of the liveness property that you try to verify, but different counter-examples may be reported.

[1] Using default settings, and ignoring effects due to parallel exploration.

On 23 Apr 2019, at 23:49, david streader <davidistreader@xxxxxxxxx> wrote:

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
VARIABLES x
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.

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