My use of terminology alas is from the refinement of Abstract data types, ADT, and process algebra so I struggle with TLA terminology but I have read the texts in quite some detail.
So a step is disabled when its guard (or precondition) is false 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.
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. 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.
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.
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. Is /\ SF_vars(Next) thought enforce strong fairness throughout the state machine?
Put another way: would SF_vars(Next) imply any other fairness condition?
It certainly is not having the effect I imagined but this may be caused by the translation from PlusCal to TLA+
regards david