I don't have time to look at the example itself, but the discussion
suggests that the problem is the confusion between a deadlocked state
and a state in which TLC reports a deadlock.
- A deadlocked state is one in which the only step allowed by the
spec's next-state action is a stuttering step--one that changes none
of the spec's variables.
- TLC reports deadlock for a state in which the next-state action allows
no step.
Thus, TLC will not report a deadlock for a deadlocked state in which
the next-state action allows a stuttering step.