Question about some concepts

[yihao yang]

Hello there,

I am learning TLA+ from Lamport's video course. I feel confused about some concepts.

Here are my questions.
1. Does deadlock mean that only the stuttering steps can be taken at the tail of the valid behaviors?
2. Is it possible to check deadlock directly by the TLA spec itself, but not by the toolbox option? What is the difference between deadlock and termination? How to specify the termination of a spec in the TLA+ spec?

Could any one give me some advices?

Thanks,
Yihao

[Leslie Lamport]

1.  Deadlock means reaching a state in which the only steps (state
changes) allowed by the spec are stuttering steps (ones that change no
declared variables of the spec).

2.  Checking the "deadlock" option in a Toolbox model tells TLC to
check for what it considers deadlock.  TLC considers a deadlocked
state to be one in which no step satisfying the next-state action Next
is possible.  The action Next is specified in the Toolbox either
explicitly in you select the "Initial predicate and next-state
relation" option for describing the behavior spec, or if you select
the "Temporal formula" by giving it a formula of the form
Init /\ [][Next]...  .  This means that TLC will not report a deadlock
in a state in which a sttuttering step satisfies the Next action.

As the video tells you, termination is deadlock that you want to
happen.  Wanting to happen means that it is deadlocked in a state that
satisfies some state predicate T that you consider to mean that the
specified system has terminated.  In that case, that a behavior
eventually terminates means that it satisfies the temporal property
<>T .  Video lecture 9 explains what you have to add to a spec if you
want it to satisfy such a property.

Leslie