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
module named 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.)
near the
part of the model containing that invariant or property.
Otherwise, the error probably occurred because TLC could not evaluate
an expression.
If you're lucky, the error message will contain the location of that
expression--or a list of locations indicating the hierarchy of
expressions that TLC was evaluating when it found the error.
Clicking on a location jumps to the appropriate point in the spec,
where that location is highlighted.
If you are model-checking a PlusCal algorithm, control-clicking on
the location will try to take you to the source of the error in
the PlusCal code.
If not lucky, you'll have to figure it out where the error occurred
from what TLC complained that it was unable to do.
If the message indicates that the error occured in a module named
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: an error-trace explorer, an 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 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.
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:
Value changed in this state.
Value added in this state.
Value removed from the next state.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 initial predicate). Double-clicking on that line takes you to the indicated location.
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.
The error-trace explorer works by running TLC on a file called TE.tla
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 MC.tla described
above. You may want to examine file TE.tla
if you can't figure out what the error in the expression is.
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
typing 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 creates a history of model runs. The history allows one to trace back the evolution of the specification and corresponding model.
Snapshots can 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.
If a TLC run completes after executing for at least this number of minutes, then the model will remain locked.
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 MC.tla and
the TLC configuration file MC.cfg when validating
the model (when you click on either run or validate).
If the spec is named SpecName
and the model is named ModName , then these two
files are written in the subfolder SpecName.toolbox/ModName .
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 @!@!@
We hope that Toolbox bugs will soon become sufficiently rare that there will be no need for the TLC Console View. You can help make that happen by reporting problems.