[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# [tlaplus] Understanding stuttering

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8889704b-d63d-492a-8fe6-902c09b15d26n%40googlegroups.com.

Attachment: stuttering.PNG
Description: PNG image