set</h3>

If TLC tries to enumerate the elements of a set, it will report an error if the set
contains more than this number of elements.&nbsp;

<h3><A name="jvmargs">JVM arguments</A></h3>

These are the arguments given to the Java Virtual Machine when TLC is run on the model.&nbsp;
Certain parameters for running TLC in
<a href="distributed-mode.html">distributed mode</a> are specified this way.&nbsp;
Only sophisticated users who know what they are doing should specify other JVM arguments.

<h3>TLC command