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.
Setting the this parameter too large may produce a Could not create the Java virtual machine error.
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 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 depth-first search, TLC will usually not produce a shortest-length error trace. When running in depth-first 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.
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.
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.
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.
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 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 |