Hi
Beginner here.
From my basic understanding, I think stuttering means that we have reached a state where we are not making any progress.
Let me know if above statements are wrong.
Context:
In below Floyd's algorithm to find cycle, i see stuttering when state(a) => CycleSize=2, Fast=0, Slow=1. In next state(b), CycleSize=2, Fast=0, Slow=0. Since Slow has changed,
Q. Is it valid to say that algorithm has stuttering at state(a).
EXTENDS Integers,
TLC \* for debugging
CONSTANTS N
VARIABLES CycleSize, Fast, Slow, Done, Steps
vars == << CycleSize, Fast, Slow, Done, Steps >>
TypeOK ==
/\ CycleSize \in 1..N
/\ Fast \in 0..CycleSize-1
/\ Slow \in 0..CycleSize-1
/\ Steps \in Nat
/\ Done \in {TRUE, FALSE}
Init ==
/\ CycleSize \in 1..N
/\ Fast \in 0..CycleSize-1
/\ Slow \in 0..CycleSize-1
/\ Done = FALSE
/\ Steps = 1
\* different starting position
/\ Fast # Slow
MovePointers ==
/\ Done = FALSE
/\ Fast' = (Fast + 2) % CycleSize
/\ Slow' = (Slow + 1) % CycleSize
/\ Done' = (Fast' = Slow')
/\ Steps' = Steps + 1
/\ UNCHANGED << CycleSize >>
Next ==
\/ MovePointers
\/ (Done = TRUE /\ UNCHANGED vars)
Spec ==
/\ Init
/\ [][Next]_vars
\* /\ WF_vars(Next)
Termination ==
<>[]Done