# Model Checking Results Page

    Contents
      General
      Statistics
      Evaluate Constant Expression
      User Output
      Progress Output

This page reports the history and status of the current or most recent execution of TLC on this model. This information is retained after TLC stops (either successfully or with an error). Even if you close the spec and open another one, or if you close the Toolbox, it will be there the next time you open the spec and this model. The information is lost only if you run TLC on the model again or delete the model or the entire spec. So, don't re-run TLC on this model until you are sure you're through examining the results of running it the last time.

Note that you can set the Toolbox to automatically snapshot (clone) the model when you re-run it. Please click the corresponding checkbox on the TLC Model Checker preference page on the File/Preferences menu. A model snapshot appears in the spec explorer tree as a child of its (parent) model. The snapshot's name indicates the date and time of its creation. Alternatively, you can manually create a clone of this model to run TLC on. (See the Models help page.)

## General

The information reported in this section is self-explanatory. See the How to run section of the Model Overview Page help page. Clicking on the Errors detected field's link raises the TLC Errors View; ignore the number of errors the field reports.

## Statistics

Two kinds of statistics are reported:

### State space progress

This shows a history of TLC's reachable state space computation. The columns have the following meanings. (See Section 14.26 [page 237] of Specifying Systems.)

Diameter
  The diameter of the reachable-state graph. It is the length of the longest behavior found so far.
States Found
  The total number of states TLC has examined so far.
Distinct States
  The number of distinct states among the states found.
Queue Size
  The number of (distinct) states found whose successor states TLC has not yet determined.

Clicking on the heading of any column displays a graph of that column's value (the vertical axis) versus execution time (the horizontal axis).

The queue size is the best guide to how far along TLC is in its computation of the reachable states. For most behavior specs, the graph of the queue size versus time is a convex curve that grows to a maximum and then decreases.

### Coverage

A common error in writing a behavior spec is for an action not to be enabled when it should be, so the spec cannot reach states that represent reachable states of the actual system being specified. This kind of error leads to a violation of desired liveness properties, but does not cause any violation of safety. The coverage statistics give you a way of catching such an error even if you're not checking liveness.

Coverage shows the number of times each sub-action of the next-state relation has been used to compute a successor state. Don't worry about how TLC decides what a sub-action is; just look at the values reported and the corresponding parts of the specification to which they refer. A sub-action that is executed zero times - emphasized by yellow background coloring of the table row - usually indicates an error in the spec. Left-clicking on an entry takes you to the indicated location.

## Evaluate Constant Expression

If you enter a constant expression in the Expression field of this section, running TLC will cause the value of that expression to appear in the Value field. The expression can use any constant operators defined or declared in the spec or elsewhere in the model. Used with the No behavior spec option on the Model Overview Page, this turns TLC into a mathematical calculator--one that computes arbitrary TLA+ expressions.

## User Output

This section shows the output generated by TLC when it evaluates `Print` and `PrintT` expressions in the spec. (A PlusCal `print` statement generates a TLA+ `PrintT` expression.) These expressions are most often used for debugging. The `Print` operator is described in Section 14.4 (page 248) of Specifying Systems; `PrintT(exp)` is defined to equal `Print(exp,TRUE)`.

## Progress Output

This section shows certain progress messages generated by TLC. All the useful information that it contains should be summarized in the General section above. However, it's possible that we've forgotten about something and that you will want to see this TLC output. Check this section if something you don't understand happens when the Toolbox runs TLC. If you don't find anything that helps you here, try the TLC Console View.

↑ Creating a Model