 line parameters</h3>

These are options given to TLC when it is run on the model.&nbsp;
A complete list of TLC options can be found in the
 <code>tlatools > src > tlc2 > TLC.java</code>
file in the
  <a href="https://github.com/tlaplus/tlaplus">GitHub repository on
  the web</a>.&nbsp;
An option specified here can override an option otherwise specified by the rest of the model,
which can cause strange things to happen.&nbsp; You should therefore use this
feature with care.


</p>

<!--  I don't know what I