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

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.

Sub-Actions of next-state

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 action statistics give you a way of catching such an error even if you're not checking liveness. 

Sub-Actions of next-state shows the number of states generated by each sub-action of the next-state relation. 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 generates no states - emphasized by yellow background coloring of the table row - usually indicates an error in the spec.  Double-clicking on an entry takes you to the indicated location. The time shown above the table indicates the execution time the numbers were recorded.

Evaluate Constant Expression

This section is described on its own page.

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