• From: Willy Schultz <will62794@xxxxxxxxx>
• Date: Sat, 18 Sep 2021 16:57:56 -0700 (PDT)

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

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"

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

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

Checking SPECIFICATION Spec causes TLC to fail with deadlock.

If I replace Next with:

Next == Pick \/ Add \/ UNCHANGED vars