Many thanks I never thought of stuttering as only occurring when a guard was satisfied that explains a lot.
If I seem to nitpicking it is just because I am not finding debugging livenes easy.
With spec
EXTENDS Naturals
VARIABLES x
Init == x=0
Inc == x<5 /\ x'=x+1
Reset == x=5 /\ x'=0
Spec == Init /\ [][Inc \/ Reset]_x
(* /\ SF_<<x>>(Inc) *)
/\ SF_<<x>>(Reset)
where stuttering is reported depends upon what property you ask as well as the spec itself.
with <> (x=2) it is after x = 1 but with <> (x=4) its is after x = 3.
Consequently it was important that I stopped interpreting it to be an improvement that the spec was not stuttering so soon.
Does the addition of liveness conditions change the State Graph to indicate where infinite stuttering might occur?