Contents Validating a Model Model Checking a Model TLC Model Checker Preferences If Something Crashes How TLC is Run The TLC Console View
You run the TLC model checker by clicking on the button. This button appears at the top of each model editor page. You can also run it from the TLC Model Checker menu or by pressing the F11 key. Before running TLC on the model, the Toolbox first validates the model, checking it for errors. Clicking on the button causes the Toobox to validate the model without running TLC on it.
The Toolbox does some validation of the model as you edit it. If that validation finds no errors, clicking on validate ( ) or run ( ) checks for other errors. The Toolbox reports any errors in the model that it finds by placing error balloons like this near the part of the model containing the error. Moving the mouse cursor on top of an error balloon will raise a message explaining the error. The Toolbox also puts an Errors Detected field at the top of the page. Moving the mouse cursor on top of it raises all the error messages for the page.
The Toolbox might report some model errors as being parsing errors in a
MC . See the section
How TLC is Run below to find out how to interpret
such an error message.
Clicking on run will cause the Toolbox to validate the model and, if it finds no errors, to run TLC on the model. The Toolbox shows the following dialog while TLC is running:
You can view the progress of the run on the model editor's Model Checking Results Page. That page is automatically displayed when TLC starts running.
Note: If you check Always run in background on the dialog shown above,
that dialog will stop popping up when you run TLC.
To get it back, go to
File/Preferences/General and uncheck the
Always run in background preference.
You can stop TLC by clicking on the Cancel button of this dialog, or else on the button that is at the top of each model-editor page, next to the run and validate buttons.
If TLC finds an error, it stops and the Toolbox raises the TLC Errors View. (If you close the view, you can reopen it from the TLC Model Checker menu.) This view consists of the following two sections. (The relative sizes of those two sections can be changed by moving the cursor between them until it changes to an up-and-down arrow, and then clicking and dragging.)
MC, see the section How TLC is Run below.
On some systems, you might find that the Error View text is displayed in an unreadably small font. See the Preferences help page to find out how to change it.
This section contains three subsections: the Error-Trace Explorer, the Error-Trace viewer, and an expression view box. The error-trace explorer can be opened or closed with the + and - symbols. The relative sizes of these subsections can also be changed by dragging the boundary between them. You can drag the entire TLC Errors view out of the Toolbox window and make it a separate window, which you can enlarge if you want to see more of the error trace at once.
The Error-Trace Explorer allows the user to add expressions which will be evaluated at each state, and whose result will be included in the output seen in the Error-Trace viewer in bold text. Expressions can be:
The error-trace explorer allows you to view the values of expressions in each step of the trace. You just enter one or more expressions, which can contain primed as well as unprimed variables, and click on Explore. The values of the expressions will then be shown in the error trace. Clicking on Restore restores the original error trace. An error-trace expression may be given the name "id" by preceding it with "id ==". This defines id to equal that expression in subsequent error-trace explorer expressions.
The error-trace explorer allows you to form expressions from two built-in operators:
_TEPosition in an error-trace expression are defined
as follows. When the expression is evaluated,
_TETrace equals the sequence of records such that
for every spec variable
v, the value of
_TETrace[N].v equals the value of v in
N of the trace. When the expression is evaluated in state number
The error-trace explorer works by running TLC on a file called
If there is an error in an expression that you entered in the error-trace
explorer, then the Toolbox may report an error in that file. The file is in the
same folder as the file
above. You may want to examine file
if you can't figure out what the error in the expression is.
The Error-Trace viewer shows a structured view of the error trace produced by TLC. The view box shows the TLA+ version of the expression selected in the error trace. (It is ordinary text that can be copied and pasted elsewhere.)
The error trace consists of a sequence of states, where a state is a TLA+ expression
that describes the values of the variables. The trace viewer provides a tree-structured
view of the state, allowing you to examine the value of each variable and of each
subexpression of that value. (Left-click on the +
and - symbols to expand and hide subexpressions.)
This is helpful in viewing complex values.
Double clicking on a state line location will open up the spec window editor and highlight that section of the spec; similar to in the Error View, holding down the CTRL, or ⌘ on macOS, key while doing this will jump to the PlusCal original code if it exists. Pressing the button with two horizontal arrows next to the 'Expand/Collapse All' button will "link" and "unlink" the trace viewer with the spec editor; when linked, a single click on a location, or using the keyboard's arrow keys, will change highlighted position like a double-click.
By default, the error trace is displayed starting with the initial state. You can reverse the order, so the initial state appears last, by clicking on either of the two column headings in the error trace display. Clicking again restores the normal order.
The trace viewer uses colors to indicate changes in the values of variables and in the values of their subexpressions from one state to the next. The color code is:
The error trace can be filtered to omit variables and expressions from the displayed states,
as well as hiding variables which have not had their values changed. By clicking on the filter button
found to the left of the expand-hide all button, the user is presented with a a dialog allowing them
to select from the set of variables and expressions found in the trace; alternatively, the user may
ALT-click on a variable or expression in the Error-Trace tree view which will then omit that
variable or expression.
On this dialog, the user may also select the visibility of the variables:
The background colors of the variables in this view change for the following cases:
The top line of a state's display in the error trace gives the location of the sub-action of the next-state
relation that generated the state (except for the first state, which is generated by the
Double-clicking on that line takes you to the indicated location.
Right-clicking on that line displays a context menu which allows the user to run model checking commencing from that described state.
The Toolbox's Preferences Menu allows you to select the following:
Controls whether or not the TLC Errors View is automatically popped up when running TLC produces an error. You will almost certainly want to use the default, which is to pop up the view.
A model is an object that is edited with a model editor. When the model is modified,
an asterisk appears in the model editor's tab, and the model can be saved by
Ctl+S. This option allows you to choose whether or not
the Toolbox should validate the model when it is saved.
The model is automatically saved when you run or validate it, so you will
probably have no reason to save it explicitly.
Re-running a model erases the corresponding model checking results if any. With snapshots activate, the Toolbox maintains a history of the N most recent model runs. The value N is defined by Number of model snapshots to keep where zero disables snapshots completely. The history allows one to trace back the evolution of the specification and corresponding model.
Snapshots can also be deleted in the Spec Explorer as needed.
This is the value to which the Maximum JVM heap size parameter of a new model is set. See the description of that parameter in the How to run? section of the model editor's Overview Page help page.
The maximum number of states of a trace that is displayed in the Trace Explorer when TLC reports an error. If the trace has more states, only the last ones are shown. Double-clicking at the beginning of the trace displays additional states. The default value is 10000.
If you stop the Toolbox in some abnormal way while it is running TLC--for example, by using an operating system tool to kill its process--you may leave TLC running as a disembodied process. In that case, you should kill the TLC process. Otherwise, strange things will happen if you restart the Toolbox and try to run TLC from it on the model.
The Toolbox runs TLC on a module named
MC that it constructs
from the model. It writes the module file
the TLC configuration file
MC.cfg when validating
the model (when you click on either run or validate).
If the spec is named
and the model is named
ModName , then these two
files are written in the subfolder
At the same time that it writes those files, the Toolbox also writes into the same
folder a copy of each of the spec's module files.
These allow you to see the version
of the spec on which TLC was run, even after you have modified the spec.
You can view that version of the spec by selecting (any page of) the model,
clicking on the
TLC Model Checker menu at the top of the Toolbox window,
and then clicking on
Open Saved Module.
It is a sad fact of life that most computer programs, including the Toolbox, have bugs. A Toolbox bug may cause TLC to stop running without either indicating that it succeeded or reporting an error. (You know that the TLC run succeeded if the General section of the Model Checking Results Page says that TLC is not running and the top entry of its Statistics section's State space progress table shows a queue size of 0.) If that page's Progress Output section doesn't explain what happened, the place to look next is the Toolbox's TLC Console View. You can open that view from the Toolbox's TLC Model Checker menu.
The TLC Console View contains all the output that TLC has produced when running this model. (You can clear the console with the view's botton.) However, each TLC output message appears between pairs of lines such as:
@!@!@STARTMSG 2200:0 @!@!@ @!@!@ENDMSG 2200 @!@!@
Toolbox bugs that would cause you to look at the TLC Console View are quite rare. You can help make that even rarer by reporting problems.