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

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




Thanks
     The error trace for safety properties has proven very helpful. But for liveness properties I had been reading to much into the trace. But won't be doing that in future.  kind regards david


On Wednesday, 24 April 2019 23:43:42 UTC+12, Stephan Merz wrote:
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.

Stephan

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

On 23 Apr 2019, at 23:49, david streader <davidis...@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 tla...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

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