VersionTag=Version 2.02 of 3 August 2009
HelpMessage=The model checker (TLC) provides the functionalities of model\n\
checking or simulation of TLA+ specifications. The syntax for this command is:\n\n\
java tlc2.TLC [GENERAL-SWITCHES] [MODE-SWITCHES] SPEC\n\n\
where SPEC is the name of the specification's root module\n\
and the optional GENERAL-SWITCHES are:\n\
 -checkpoint num: interval between check point (in minutes)\n\
 \tDefaults 30 if not provided.\n\
 -cleanup: clean up the states directory\n\
 -config file: provide the config file.\n\
 \tDefaults to SPEC.cfg if not provided\n\
 -continue: continue running even when invariant is violated\n\
 \tDefaults to stop at the first violation if not specified\n\
 -coverage minutes: interval between collection of coverage information \n\
 \ton the spec in minutes. Defaults to no coverage if not specified\n\
 -deadlock: do not check for deadlock.\n\
 \tDefaults to check deadlock if not specified\n\
 -difftrace: show only the differences between successive states,\n\
 \twhen printing trace. Defaults to print full state descriptions\n\
 -debug: debugging information (not for production use)\n\
 -dump file: dump all the states into file\n\
 -fp num: use the num'th irreducible polynomial from the list \n\
 \tstored in the class FP64.\n\
 -gzip: control if gzip is applied to value input/output stream.\n\
 \tDefaults to use gzip.\n\
 -metadir path: store metadata in the directory at path\n\
 \tDefaults to SPEC-directory/states if not specified\n\
 -recover id: recover from the checkpoint with id\n\
 \tDefaults to scratch run if not specified\n\
 -terse: do not expand values in Print statement\n\
 \tDefaults to expand value if not specified\n\
 -tool: tool mode (put message codes on console)\n\
  -nowarning: disable all the warnings.\n\
 \tDefaults to report warnings if not specified\n\
 -workers num: the number of TLC worker threads. Defaults to 1.\n\n\
By default, TLC starts in the model checking mode using breadth-first\n\
approach for the state space exploration. This can be changed using\n\
the MODE-SWITCHES. In contrast to the GENERAL-SWITCHES these can be used \n\
if applied in certain combinations only:\n\n\
{[-dfid num][ -view]|-simulate[ -depth num][ -aril num][ -seed num]}\n\n\
 -modelcheck: run in model checking mode using breadth-first approach for the\n\
 \tstate space exploration (default)\n\
 -dfid num: run in model checking mode and use depth-first iterative deepening\n\
 \twith initial depth num\n\
 -view: apply VIEW (if provided) when printing out states.\n\
 -simulate: run in simulation mode\n\
 -depth num: specify the depth of random simulation\n\
 \tDefaults to 100 if not specified\n\
 -seed num: provide the seed for random simulation\n\
 \tDefaults to a random seed if not specified)\n\
 -aril num: Adjust the seed for random simulation\n\
 \tDefaults to 0 if not specified\n\