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 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.
This section is described on its own page.
This section shows the output generated by TLC when it evaluates
PrintT expressions in the spec. (A PlusCal
PrintT expression.) These expressions are most often used
for debugging. The
PrintT(exp) is defined to equal