TLC Options Page

Contents
  Configuration
  Checking Mode
  Features
  Parameters

This model editor page allows you to add less-often used parts of a model.  It's a good idea to browse this page just to see what options it provides, since some of the features are not ones you would expect.

Configuration

Number of worker threads

TLC's algorithm for computing the set (actually the graph) of reachable states is highly parallelizable, and it can make good use of arbitrarily many processors.  This parameter specifies the number of separate threads that TLC will spawn to perform that computation.  You should not set it to be greater than the number of separate processors (cores) on your computer; the Toolbox will warn you if you do. When using multiple workers on a medium-small model, the reported Diameter might differ across runs. This is a limitation we accept to avoid putting additional synchronization that would limit the scalability. For small models, use a single worker. For large models, the diameter will almost always appear deterministic.

Fraction of physical memory allocated to TLC

This determines how large a heap TLC will use.  If you make it too small, TLC could run out of heap space and crash.  If you make it too large, your machine will not have enough memory and everything will run slowly.  The slider's color warns you if you are giving TLC too little or too much memory.  TLC can keep the set of reachable states it has found on disk, so having too many reachable states can't run it out of memory.  However, it runs much faster when it can keep those states in memory.  TLC can run out of heap space if it takes too much memory to represent the set of initial states or the set of successor states of a single state.  If TLC does run out of memory in the middle of a long run, you can give it more and restart it from a checkpoint.

Setting the this parameter too large may produce a Could not create the Java virtual machine error.

Log base 2 of number of disk storage files

If your computer has multiple disk drives, setting this parameter to a value greater than 0 might make it possible to reduce the time TLC spends writing to disk on a model with a very large number of reachable states.  Contact us for more information.

Saving defaults

Clicking on the "Save as default" button in this section will save this configuration and use it as the configuration in new models.

Checking Mode

You can choose between two basic ways of running TLC:

Model-checking mode

This is the normal method of running TLC, in which it essentially tries to check all possible behaviors allowed by the behavior spec.  Its default method of doing this is to find the graph of all reachable states using breadth-first search.  This has the advantage that if TLC finds a violation of a safety property, then it will produce a shortest possible behavior that exhibits the error.  You can direct TLC to use a depth-first iterative deeping (DFID) search by choosing the Depth-first option and specifying the depth of its search.  (Limiting the depth ensures that only a finite set of states is explored, even if the complete set of reachable states is infinite.)  With DFID search, TLC will usually not produce a shortest-length error trace.  When running in DFID mode, TLC does not compute the entire state graph and does not use a state queue, so it does not produce any Diameter or Queue size statistics. Additionally, the DFID option doesn't currently support running with multiple workers.

Warning: Depth-first search is an experimental TLC option that has not been used much. We don't know if it offers any advantages. If you do try it and find it useful, please tell us what you did.

You can also specify a View to be used in model-checking mode.  If you're curious about what that is and how it is used, see Section 14.3.3 (page 243) of Specifying Systems.

Simulation Mode

In simulation mode, TLC does not try to examine all reachable states.  Instead, it checks an unending series of behaviors, each of which it constructs by starting from a randomly choosen initial state and repeatedly making a random choice of a possible next state.  (In this mode, you stop TLC by clicking the  Cancel  button on the dialog that the Toolbox pops up when it runs TLC.)  You specify the maximum length of each behavior that it generates.  If you want to know what specifying the Seed and Aril does, look them up in Specifying Systems.  When run in simulation mode, the only statistics TLC reports are for States Found.

Features

Checkpoint Recovery

TLC takes regular checkpoints, from which it can be restarted if it is stopped for any reason--for example, if your computer crashes.  The Recover from checkpoint option tells TLC to start from where it was when the last checkpoint was taken.  This option is enabled if the last time you ran TLC, it ran long enough to produce a checkpoint.  The Toolbox will fill in the Checkpoint id for you.

Warning: If you exit the Toolbox, it will stop any executions of TLC that are in process.  However, it is possible to stop the Toolbox in some drastic fashion that leaves TLC running as a background process.  Restarting from a checkpoint while the TLC process that created it is still running can cause the checkpoint to be destroyed, making recovery impossible.  If you have reason to believe TLC was not stopped, check to see if it is still running before trying to recover from a checkpoint.

The checkpoint TLC produces after a short run does not take up much space.  However, if TLC finds an error after running for a long time, the checkpoint files could take up a lot of space--sometimes on the order of a gigabyte for a model that has run for several days.  These files are deleted if the model is re-run and a new checkpoint is produced, or if the model is validated when the Recover from checkpoint option is not selected.  When TLC has created a checkpoint, the Features section of the TLC Options page displays how much storage the checkpoint occupies.  It also provides a button that you can click to delete the checkpoint. 

Checkpointing does not yet work when TLC is run in distributed mode.

Profiling

TLC supports detailed profiling at the action as well as the expression level. Profiling helps to identify specification errors such as permanently disabled actions (compare Enabled predicate in The Temporal Logic of Actions section 2.7, page 6). Similarly it helps pinpoint the source of state space explosion by reporting the states found and distinct states on a per action level.

In addition to action profiling, invocation and cost profiling allows to diagnose expensive expressions. Please refer to the dedicated profiler documentation for more information.

Warning: Profiling negatively impacts model checking performance and should thus be off when checking large models.

Visualize state graph after completion

Visualize the generated state graph graphically after completion of model checking. The visualization helps to better understand the system being specified. Initial states are represented by gray vertices.

Warning: Can reasonably display only state graphs with at most around a hundred states.

In order to visualize a state graph, the path to the dot executable of the GraphViz project has to be set under Specify dot command on the PDF viewer preference page on the File/Preferences menu. On macOS dot is most easily installed with the ports system. Homebrew has a Graphviz port too. On Windows, GraphViz can be obtained through Cygwin or installed standalone. On most Linux derivatives, GraphViz can be installed with the package manager. After installation, the dot binary can usually be found at:

OS Default path
Windows (Cygwin) C:\cygwin\bin\dot.exe
Windows (standalone) C:\Program Files (x86)\Graphviz2.38\bin\dot.exe
macOS (ports) /opt/local/bin/dot
Linux /usr/bin/dot

On Windows and Linux the state graph will be visualized with either the built-in or standalone PDF viewer depending on which is selected on the PDF viewer preference page (selecting a standalone viewer is advised for best results).

Parameters

Verify temporal properties upon termination only

Defer the verification of temporal properties (liveness) to the end of model checking. This reduces the overall model checking time with the additional side effect that invariant (safety) violations will always be found first. In other words, check liveness only after the complete state space has been checked for safety violations. If unchecked, temporal properties are checked periodically on the incomplete state graph. Deferring verification of temporal properties is especially useful if it is highly likely that the model does not violate its temporal properties (e.g. a smaller instance of the model has successfully been verified for liveness violations).

Fingerprint seed index

TLC saves only 64-bit fingerprints (hashes) of the reachable states that it finds, not the complete states.  If two different reachable states have the same fingerprint, a situation called a collision, TLC may not find all reachable states.  At the end of a run, TLC prints estimates of how likely it was that a collision occurred.  If you're worried that a collision might have occurred, you can re-run the model with a different fingerprint function.  The fingerprint seed index specifies which of 64 fingerprint functions TLC should use.  If the two runs produce different numbers of reachable states, then there was a collision in at least one of the runs.  If not, the probability that there was a collision in both is the square of the probability that either one had a collision--a probability that is probably very, very small.  By default, which fingerprint function to use is chosen randomly.

Cardinality of largest enumerable set

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. 

JVM arguments

These are the arguments given to the Java Virtual Machine when TLC is run on the model.  Certain parameters for running TLC in distributed mode are specified this way.  Only sophisticated users who know what they are doing should specify other JVM arguments.

TLC command line parameters

These are options given to TLC when it is run on the model.  A complete list of TLC options can be found in the tlatools > src > tlc2 > TLC.java file in the GitHub repository on the web.  An option specified here can override an option otherwise specified by the rest of the model, which can cause strange things to happen.  You should therefore use this feature with care.

↑ Creating a Model