confusion about stuttering / deadlock

[Pablo Fernandez]

Given this spec

----------------------------- MODULE PickAndAdd ----------------

EXTENDS Integers, TLC

VARIABLES pc, i

vars == <<pc, i>>

Init == /\ i = 0

        /\ pc = "start"

Pick == /\ pc = "start"

        /\ i' \in 1..10

        /\ pc' = "middle"

Add == /\ pc = "middle"

       /\ i' = i + 1

       /\ pc' = "done"

Next == Pick \/ Add

Spec == Init /\ [][Next]_vars

================================================================

Checking SPECIFICATION Spec causes TLC to fail with deadlock.

If I replace Next with:

Next == Pick \/ Add \/ UNCHANGED vars

The deadlock error goes away.

My questions are: 

1. isn't that UNCHANGED what the [][Next]_vars is supposed to do? 

2. why do I have to add the extra UNCHANGED statement? 

3. Is there a convention or a better way to check for program termination?

Thanks!

[Willy Schultz]

In TLA+, a behavior is defined as exhibiting a "deadlock" if it reaches some state for which there is no (non-stuttering) transition that is enabled (see Specifying Systems[1], page 222). More precisely, it is a state for which there is no transition of Next that can be taken. That is, 

~(ENABLED Next) 

holds. In your specification as written, once you reach a state where pc="done", there will be no enabled transitions leaving that state. So, by definition, such a state is considered a deadlock. Now, in many cases this does not actually indicate an error. It just means that the system terminated correctly. So, it is relatively common to disable deadlock checking in TLC by default (see the -deadlock flag) and then define your own termination conditions as needed. For example, a valid termination condition of your spec may be something like 

(pc="done") => (i \in 2..11)

In general, when writing specs in TLA+, you may need to specify explicitly what it means for a state to be a "valid" terminal state. You can then use TLC to check this condition just as you would any other invariant. Adding the extra UNCHANGED statement as you did is, as far as my understanding goes, somewhat of a bad practice, since you may indeed want to check for deadlock states (as defined above) in certain situations.

Will

[1]  https://lamport.azurewebsites.net/tla/book-02-08-08.pdf

[Stephan Merz]

Simply to add to Will's answer, introducing an extra action that leaves all variables unchanged when the algorithm has terminated is in fact exactly what the PlusCal translator does. It is a way of explicitly stating that stuttering should not be considered a deadlock in such a situation. For your specification, you could write

Next == Pick \/ Add \/ (pc = "done" /\ UNCHANGED vars)

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/ccdfbe8e-da12-4f69-8c20-a7c3c3a11c8en%40googlegroups.com.

[Pablo Fernandez]

Thanks Will and Stephan for your answers.

Is it OK then to say that [][Next]_vars will allow stuttering but that stuttering must happen on a valid state, and no valid state matches pc = "done"? or, to say it otherwise, there's no possible stuttering on pc = "done" since that state is not modelled in the spec?

[ns]

I'm not sure what you mean by no valid state matches 'pc=done'. TLA defines deadlock as happening when no action is enabled. When you omitted the "UNCHANGED var"  action, there was indeed no action enabled once the pc had reached the done state. However adding that action meant that at least one action was always enabled, hence no deadlock. What may be confusing is that the 'UNCHANGED vars' action looks like the machine stuttering, which can happen at any state, and does not require any specific action (that's why TLA formulas are stuttering invariant). This all becomes clearer if you adopt Stephan's suggestion. Without Stephan's modification, the system can simply repeat the 'UNCHANGED vars" action forever and never carry out Pick or Add. But with his change, you'll see that the system only carries out the UNCHANGED vars action in the done state, whereas stuttering can happen in any of the states. Finally, TLC does give you the option of turning off deadlock checking in cases where your system is meant to terminate, but I find that somewhat risky since it also means that it won't detect actual (undesirable) deadlock that may be lurking elsewhere in your spec

--ns