| 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
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
On Saturday, September 18, 2021 at 5:28:00 PM UTC-4 fernande...@ gmail.com 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.
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/0E5ECB7C-BDF7-4F56-98E8-35B8281D1BD8%40gmail.com.
|