Re: [tlaplus] Understanding stuttering

Stephan

On 20 Nov 2020, at 10:35, Ashish Negi <thisismyidashish@xxxxxxxxx> wrote:

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 ?

On Thu 19 Nov, 2020, 11:51 PM Stephan Merz <stephan.merz@xxxxxxxxx wrote:
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

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>

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1EDD6030-F52F-464D-9459-EA1350C66F4F%40gmail.com.

--
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/CAMo8VbF9tnjx4xcRm6e3K2Qy0qbzm%3DqSU0LMecQBnJ8-Wk4vnA%40mail.gmail.com.