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