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

Re: [tlaplus] Understanding stuttering



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 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/1EDD6030-F52F-464D-9459-EA1350C66F4F%40gmail.com.