On Saturday, 30 March 2019 20:43:56 UTC-4, david streader wrote:
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.
`Inc` can only be "chosen" when its guard is true (the typical parlance is to say that `Inc` is "enabled" or "not enabled/disabled"). When its guard is false (i.e., whenever x is not less than 5), an Inc step cannot take place.
So what can take place when `Inc` is not enabled? When x=5, a `Reset` step _could_ take place. But there's no guarantee that it will take place, and thus stuttering is possible. In other words, when x=5, the `Reset` step is enabled, but because there's no fairness associated with that step (either weak fairness or strong fairness), we aren't requiring that the step eventually be taken
Stuttering steps are steps in which no variables in the formula change. The rest of the universe happily moves along during those steps, but _your_ particular variables remain unchanged. In a real system, this might represent a process having received a message (and thus its guard/enabling condition being true), but it never responds because the operating system scheduler doesn't give the process time on the CPU.
Or it could even represent a process receiving a message, but never responding, because the process crashes! If `Reset` represents a process in your system, and it's supposed to "do its thing" whenever x=5, what happens if `Reset` process crashes? Nothing! It sits there stuttering. But this is NOT deadlock, because _mathematically_ there's a way for the system to proceed, for the system to move to a different step. And all deadlock checking cares about is whether or not there's a transition out of a state.
This system WILL deadlock, because once it reaches x=5, there's no transition out of the state.
```
Init == x=0
Inc == x<5 /\ x'=x+1
Spec == Init /\ [][Inc]_x /\ WF_x(Inc)
```
If you disable deadlock checking, and run it with a check for temporal property []<>(x=1), then it too will report stuttering at the state x=5.
Is it reasonable to say that a particular step, Inc in this example, is the stuttering step??
Nope. `Inc` may stutter for some period of time (for a million years even), but by saying `WF_x(Inc)`, we're saying that _eventually_ the `Inc` step will take place when `Inc` is enabled.
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?
The dashed loop arrows are (I believe) indicating stuttering steps. Any one of those states can stutter, but for the states where x is one of 0..4, your system can't stutter _infinitely_.
Your weak fairness condition of WF_x(Inc) states that if `Inc` ever becomes enabled forever, then the `Inc` step will eventually take place. When, for example, x=3, your process could sit for a LONG time doing nothing (i.e., stuttering), but WF means that _eventually_ the step will take place and you'll go to x=4. And TLC only throws an error when a behaviour can _infinitely_ stutter.
But you have no such fairness condition for the time at which x=5. In that case, your process may be enabled infinitely, and never proceed, and thus TLC gives the stuttering error.
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?
The behaviour that stutters infinitely is
x=0 -> x=1 -> x=2 -> x=3 -> x=4 -> x=5 [stutters here forever]
That's not the ONLY possible behaviour your system can experience. A _possible_ behaviour is that after some time with x=5, the `Reset` action is allowed to take place, setting x back to 0. But because you haven't specified fairness on `Reset`, it's _possible_ for it to sit there stuttering forever, and thus the temporal property is violated.
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) ??
Any system can stutter at any point in time, for potentially an infinite amount of time. But if you don't specify any temporal properties in the model checker, then TLC won't check for stuttering.
When you enable a temporal property for checking, then TLC finds the state x=5 allows for infinite stuttering.
The reason that x=2 does NOT falsify []<>(x=0) is because the system won't infinitely stutter at that state, thanks to your WF_X(Inc). You are guaranteeing that your system will always progress forward from that point. But once it hits x=5, there's no more guarantee, as it can stutter infinitely there.
So do the dashed loops on the State Graph indicate that it can stutter from any state
I believe they indicate it can stutter from any state, but NOT that it will _infinitely_ stutter from that state.
My intuition was that
Spec == Init /\ [][Inc \/ Reset]_x /\ SF_x(Inc) /\ SF_x(Reset)
would not stutter and experimentation confirmed this.
You could also have done
Spec == Init /\ [][Inc \/ Reset]_x /\ WF_x(Inc) /\ WF_x(Reset)
Strong fairness is harder to implement in practice, so it's usually best to start with weak fairness.
The notions of stuttering and fairness are not intuitively obvious, in my experience. You'll likely have to read through the relevant parts of "Specifying Systems" (https://lamport.azurewebsites.net/tla/book-02-08-08.pdf) to really get a handle on them.
In particular, chapter 2 introduces stuttering very early on, and chapter 8 gives much more elaborate and formal definitions. These concepts personally took me a decent chunk of time to understand, with lots of staring at the page and re-reading the same paragraphs over and over.