# Checking a Model

    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.

## 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, 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.

#### The Trace View

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.

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

### Take snapshot of model after completion of model checking

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.

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

### TLC Run Auto-Lock Time

If a TLC run completes after executing for at least this number of minutes, then the model will remain locked.

### 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 @!@!@

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.

↑ Model Checking