Re: [tlaplus] Understanding stuttering

It may appear silly to allow stuttering steps to occur as long as you consider only one algorithm at a single level of abstraction but it turns out to be an essential concept for representing composition and refinement using conjunction and implication. The underlying philosophy is that a TLA+ specification describes an entire universe that contains the system that you are describing, and in that universe many events take place besides those that correspond to system steps.

On 19 Nov 2020, at 23:52, thisismy...@gmail.com <thisismyidashish@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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8889704b-d63d-492a-8fe6-902c09b15d26n%40googlegroups.com.
<stuttering.PNG>