[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 Stephan. 
       
So with
Init == x=0
Inc == x<5 /\ x'=x+1
Reset == x=5 /\ x'=0
Spec == Init /\ [][Inc \/ Reset]_x /\ WF_x(Inc)
Is it correct to say that when the the guard (x<5) is false it does not prevent the step Inc from being  chosen. But if Inc is chosen and the guard is false then the system stutters.
Is it reasonable to say that a particular step, Inc in this example, is the stuttering step??

The error trace clearly indicates that stuttering occurs form state (x=5)  but there is nothing on the State Graph to indicate that stuttering is possible from state (x=5) and not from other states. There are dashed loop arrows from every state. These loops do not seem to be related to any particular step. Do you know what they indicate?


You say 
However, it fails to satisfy the property  []<>(x=0)  because there is a behavior that stutters infinitely at the state where x=5: since Inc is disabled at that state,

But Reset is disabled when x=1 does this lead to stuttering?

I experimented with []<>(x=3)  e.t.c. The results surprised me.  I think of stuttering as a property of the State Machine but where stuttering is reported depends upon the property checked not upon the State machine itself. Am I mistaken to think of stuttering as a property of the state machine? If stuttering is a property of the State Machine then I would have thought that stuttering from the State (x=2) would  also falsify []<>(x=0)  ??

So do the dashed loops on the State Graph indicate that it can stutter from any state

My intuition was that
 Spec == Init /\ [][Inc \/ Reset]_x /\ SF_x(Inc) /\ SF_x(Reset)
 would not stutter and experimentation  confirmed this.

Hope my questions make sense in TLA+ terms because i feel that I am approaching TLA+ with a lot of intellectual baggage. 

kind regards david 

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