 and does not use a state
queue, so it does not produce any
 <i>Diameter</i> or <i>Queue size</i>
 statistics.
Additionally, the DFID option doesn't currently support
running with multiple workers.
</p>
<p>
<b>Warning:</b> Depth-first search is an experimental TLC
option that has not been used much. We don't know
if it offers any advantages.
If you do try it and find it useful, please tell us what you did.
</p>

<p>
You can also specify a <em>View</em> to be used in model-checking
mode.&nbsp;  If you're cur