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