[tlaplus] Re: confusion about stuttering / deadlock

[Willy Schultz <will62794@xxxxxxxxx>]

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

On Saturday, September 18, 2021 at 5:28:00 PM UTC-4 fernande...@xxxxxxxxx wrote:

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!

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