bsp;  (In this mode, you  stop TLC by clicking the&nbsp;
<samp>Cancel</samp>&nbsp; button on the dialog that the Toolbox pops up when it
runs TLC.)&nbsp; You specify the maximum length of each behavior that it generates.&nbsp;
If you want to know what specifying the <em>Seed</em> and <em>Aril</em> does,
look them up in
<em><a href=
"http://research.microsoft.com/en-us/um/people/lamport/tla/book.html" target="_blank">
Specifying Systems</a></em>.&nbsp;  When run in simulation mode, the only
statistics TLC re