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