Checking a Model

  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.

Validating a Model

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.

Model Checking a Model

Starting TLC

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.

Stopping TLC

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.

TLC Error Reports

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.)

The Error View

This view displays the error message that TLC reports.  If an invariant or property is violated, the Toolbox will also put this warning icon 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, CTRL-clicking, or ⌘-clicking on macOS, 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.

The Trace View

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:

If at least one expression is enabled, the "Explore" button will be enabled; clicking this button will run the model checking including the evaluation of the enabled expressions.
After a checking has been run including evaluated expressions, the list of expressions and "Add," "Edit," and "Remove," will be disabled until the user clicks on the "Restore" button.
Additionally, formulas may be drag-reordered in the list.

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: The operators _TETrace and _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 state number N of the trace. When the expression is evaluated in state number N, the operator _TEPosition equals N.

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 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:

While variables are being filtered, a checkbox will be displayed above the variable value viewing text area allowing this area to display all the variables, or only the filtered variables, when a state is selected in the Error-Trace tree.
Clicking on the filter button again will turn off the filtering.

The background colors of the variables in this view change for the following cases:

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.
Right-clicking on that line displays a context menu which allows the user to run model checking commencing from that described state.

TLC Model Checker Preferences

The Toolbox's Preferences Menu allows you to select the following:

Always pop up TLC errors view

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.

Re-validate model on save

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.

Number of model snapshots to keep

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.

Maximum JVM Heap Size

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.

Default number of states shown in error traces

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 Something Crashes

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.

How TLC is Run

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.

The TLC Console View

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.

↑ Model Checking