TLC's Command-Line Options

Leslie Lamport

Last modified on 21 December 2018


You'll miss a lot on this web site unless you enable Javascript in your browser.

  • -config file  Provide the config file.  Defaults to spec.cfg if not provided

  • -deadlock  Do not check for deadlock.  Defaults to checking deadlock if not specified. 

  • -depth num  Specify the depth of random simulation.  Defaults to 100 if not specified.

  • -seed num  Provide the seed for random simulation.  Defaults to a random seed if not specified.

  • -aril num  Adjust the seed for random simulation.  Defaults to 0 if not specified.

  • -recover path  Recover from the checkpoint at path.  Defaults to starting a new run if not specified.

  • -bound  The upper limit for sets, effectively limiting the number of init states (see http://bugzilla.tlaplus.net/show_bug.cgi?id=264).  Defaults to 1000000 if not specified.

  • -metadir path  Store metadata in the directory at path.  Defaults to specdir/states if not specified.

  • -userFile file  A full qualified/absolute path to a file in which to log user output (for example, produced by Print).

  • -workers num  The number of TLC worker threads.  Defaults to 1.

  • -dfid num  Use depth-first iterative deepening with initial depth num.

  • -cleanup  Clean up the states directory.

  • -dump file  Dump all the states into file.

  • -difftrace  When printing an error trace, show only the differences between successive states.  Full state descriptions are printed if not specified.  (Added by Rajeev Joshi.)

  • -terse  Do not expand values in Print statement.  Defaults to expand values if not specified.

  • -coverage min  Collect coverage information on the spec, print out the information every min minutes.  Defaults to no coverage if not specified.

  • -continue  Continue running even when invariant is violated.  Defaults to stop at the first violation if not specified.

  • -nowarning  Disable all warnings.  Defaults to report warnings if not specified.

  • -fp num  Use the irreducible polynomial number num from the list stored in the class FP64.

  • -view  Apply VIEW (if provided) when printing out states.

  • -gzip  Control if gzip is applied to value input/output stream.  Defaults to use gzip.

  • -debug  Debbuging information (non-production use).

  • -tool  Tool mode (put output codes on console).

  • -checkpoint num  The length of time between checkpoints (in minutes).  Defaults to 30.

  • -fpmem num  The number of megabytes of memory used to store the fingerprints of found states.  Defaults to 1/4 physical memory. (Added 6 Apr 2010 by Yuan Yu.)

  • -fpbits num  The number of msb used by MultiFPSet to create nested FPSets.  Defaults to 1.

  • -maxSetSize num  The size of the largest set TLC will enumerate.  The default value is 1000000.