[tlaplus] confusion about stuttering / deadlock

[Pablo Fernandez <fernandezpablo85@xxxxxxxxx>]

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/63a1beeb-32f6-4bef-88b9-c9ef4083db8cn%40googlegroups.com.