David,
So a step is disabled when its guard (or precondition) is false
Correct
and although we don't say that it is the particular step that stutters it is when a guard evaluates to false that stuttering occurs.
Incorrect. Stuttering is when a step is enabled (i.e., its guard/precondition/enabling-conditions are true), but instead of the step being taken, _nothing at all happens_. And by "nothing at all happens", very strictly, I mean that _all_ the variables defined with VARIABLES remain unchanged.
Stuttering in and of itself is completely fine. Everything stutters all the time. Stuttering means that the infinite numbers of other variables in the universe may or may not be changing in between two distinct points in time, but _our_ variables defined with VARIABLES remain unchanged. And this is expected. As one example, if you're running a process on a single core CPU, the operating system is putting your process on and off the core all the time. Whenever it's off the core, you could think of your software as stuttering. The universe continues to move forward, but the state of your process remains the same. The question is, does your spec guarantee that your process will _eventually_ run again. (Naturally it's more subtle than that, but hopefully that helps with understanding/terminology).
Every spec we write, every program we write, it all is going through stuttering all the time. That's fine and expected.
But the problem is when a particular spec might _infinitely stutter_. From a terminology point of view, we must understand that stuttering is fine and normal, but infinite stuttering is what temporal properties are generally concerned with. And TLC will _only_ check for infinite stuttering if you explicitly instruct it to check a temporal property. TLC calls the error "stuttering", but really it means "infinite stuttering".
With no fairness condition Spec == Init /\ [][Inc \/ Reset]_x then the state machine we considered
Init == x=0
Inc == x<5 /\ x'=x+1
Reset == x=5 /\ x'=0
could stutter immediately and falsify any liveness condition.
Correct. When x=0, the system can stutter (just like it can at x=1, x=2, ...). Since we have no fairness specified, we have no guarantee that the stuttering will _eventually_ cease, and thus TLC raises the error.
But the error trace displayed depends on the temporal condition, it may first completes several steps before stuttering even though it could stutter immediately and falsify the condition. I misinterpreted the error trace as implying that this was the first point that stuttering could occur where as I gather that this is the first point where stuttering is checked.
For the original spec you posted (with fairness on Inc but not on Reset), then x=5 _is_ the first place that "infinite stuttering" could occur.
But with no fairness specified, the point at which the stuttering error is raised is an implementation detail. With no fairness condition specified, then the following could _also_ be raised as a stuttering error
x = 0 -> x = 1 [stuttering]
But the nature of TLC means that it "discovers" the stuttering problem at x=0, and stops right there.
TLA+ allows fairness to be defined for very specific situations but because of my background in process algebra and abstract data types all I want is to have strong fairness every where. In ADT and process algebras CSP and CCS nothing stutters by default you have to add some thing to enable stuttering.
The easiest way to do this is to not check for temporal properties :) But once you start checking for temporal properties, then TLC wants to find if any otherwise valid behaviours might infinitely stutter.
I gather /\ WF_vars(Next) is will stop all stuttering but not sure what the effect of restricting the vars to a subset of the variables is.
(I think it's an error to restrict WF to a subset of variables, but someone more knowledgable can correct me.)
Well, it won't necessarily stop all stuttering. `WF_vars(Next)` means that if a condition is "enabled forever", then the step will eventually take place. But you can have behaviours where a condition is enabled and then disabled and then enabled and then disabled, ad nauseam, which would result in a violation of some temporal properties.
In either part 1 or part 2 (http://lamport.azurewebsites.net/video/video9a.html or http://lamport.azurewebsites.net/video/video9b.html) of Lamport's "Alternating Bit Protocol" video lecture, he has a great example showing this taking place. I recommend watching both videos (and the entire series, in fact http://lamport.azurewebsites.net/video/videos.html)
Is /\ SF_vars(Next) thought enforce strong fairness throughout the state machine?
SF_vars(Next) means that if a condition is infinitely enabled and disabled, then the step will eventually take place.
Take this modified spec as an example
```
EXTENDS Integers
VARIABLES x
Init == x=0
Inc == x<5 /\ x'=x+1
Reset == x \in {5, 6} /\ x' = 0
JumpToSix == x = 5 /\ x' = 6
Next == Inc \/ Reset \/ JumpToSix
Spec == Init /\ [][Next]_x /\ SF_x(Next)
```
Set a temporaral property of `[]<>(x=6)`. You will have a stuttering violation. Even though we have SF_x(Next), we're not guaranteed to ever take the JumpToSix step.
If we change Spec to:
Spec == Init /\ [][Next]_x /\ SF_x(Inc \/ Reset) /\ SF_x(JumpToSix)
Then the stuttering violation is eliminated.
But try changing those SF_x to WF_x and see what happens!
Put another way: would SF_vars(Next) imply any other fairness condition?
If something is satisfied by weak fairness, then it is also satisfied by strong fairness.
It certainly is not having the effect I imagined but this may be caused by the translation from PlusCal to TLA+
There are definitely places in the way PlusCal is translated in which fairness can get especially tricky. You can mark the whole algorithm as fair (which might not do exactly what you expect), you can mark an individual process as fair (which also might not do what you expect), and you can even mark individual labels as fair. See page 38 of https://lamport.azurewebsites.net/tla/p-manual.pdf