Understanding stuttering

[thisismy...@gmail.com]

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

[thisismy...@gmail.com]

Next ==
    \/ MovePointers

    \/ (Done = TRUE /\ UNCHANGED vars)

Or

Next ==
    MovePointers

makes no difference.

[Stephan Merz]

The basic form of a TLA+ specification is

Init /\ [][Next]_vars

and this allows for stuttering to occur at any state, even indefinitely, since [Next]_vars is shorthand for

Next \/ UNCHANGED vars

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.

The upshot is that you need to add fairness conditions if you want to ensure the system to make progress. For more information, please watch lecture 9 of the TLA+ video course.

Stephan

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

[Ashish Negi]

Ok. For my other beginner specs I didn't see this problem because I was using Model Checker view where I gave Init and Next states. Now I was specifying my Spec action. 

Was TLC additing WF in first case automatically ?

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/XuDsRElDEHc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1EDD6030-F52F-464D-9459-EA1350C66F4F%40gmail.com.

[Stephan Merz]

I presume you did not check any liveness properties for your other specs?

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAMo8VbF9tnjx4xcRm6e3K2Qy0qbzm%3DqSU0LMecQBnJ8-Wk4vnA%40mail.gmail.com.

[recepient recepient]

https://www.hillelwayne.com/post/fairness/ from Hillel Wayne whose Practical TLA+ book (on Amazon among others) I recommend does a very nice job at explaining stuttering. 

[thisismy...@gmail.com]

yes, i didn't play with liveness properties before.

thanks for sharing hillelwayne article. It cleared things.