a name="checking">Checking Mode</a></h2>

You can choose between two basic ways of running TLC:

<h3><a  name="model-mode">Model-checking mode</a></h3>
<p>
This is the normal method of running TLC, in which it
essentially tries to check all possible behaviors allowed
by the behavior spec.&nbsp;  Its default method of doing this
is to find the graph of all reachable states using
breadth-first search.&nbsp;  This has the advantage that if
TLC finds a violation of a safety property, then it will
produce a shor