# [tlaplus] Re: Understanding stuttering

Next ==
\/ MovePointers
\/ (Done = TRUE /\ UNCHANGED vars)

Or

Next ==
MovePointers

makes no difference.

On Thursday, 19 November 2020 at 14:52:21 UTC-8 thisismy...@xxxxxxxxx wrote:
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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.