[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Question about some concepts

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.