1 Checking Termination
In this tutorial, we consider two correctness properties of a program
that is supposed to compute a value and terminate: that it computes
the correct value and that it terminates. You have seen how to
Open the specification
Open that model and on the Model Overview tab, open the
Properties part of the What to check? section. As
shown here, the default is not to check for termination. Check
the box next to Termination and run TLC on the model. TLC
raises an error window reporting that
As indicated on the screen shot, termination is the only temporal
property. So, algorithm
The question I would ask is, why did the execution get that far?
The answer is that, while TLC generally reports a shortest execution
in which an algorithm terminates with the wrong answer,
for uninteresting technical reasons
it often does
not report the shortest possible non-terminating execution.
This seems crazy. Why doesn't PlusCal require that an algorithm keep going until it terminates (or deadlocks)? This requirement is an example of a class of requirements called fairness conditions. It is generally assumed without mention for uniprocess algorithms. However, we don't always want to require it for multiprocess algorithms. For example, consider an algorithm in which a client process issues requests to which a server process responds. Requiring execution not to stop if the system hasn't terminated (or deadlocked) would mean that the client could never stop issuing requests, something we might not want to require. So, we don't want this requirement to be the default.
We add the requirement to an algorithm by replacing
now make the algorithm run forever. Comment out the statement
2 TLC's State Graph
No execution of this modified version of
The answer is that TLC does not compute executions; it computes reachable states. More precisely it computes a graph whose nodes are all states that can occur in some execution and whose edges describe the possible transitions from one state to the next state. Here is the graph for this algorithm, where the shaded node describes the initial state:
Here is the state graph for
the original version of our
algorithm, with the
Termination is halting when we want the algorithm to halt. Deadlock is halting when we don't want it to halt. Wanting does not appear in a mathematical view of an algorithm. The transition from the terminating state to itself is added to the TLA+ translation of the algorithm so TLC doesn't consider termination to be deadlock.
most algorithms, there are much too many reachable states for a
picture of the state graph to be useful.
However, looking at a tiny state graph can help you understand
To find the number of reachable states TLC has found, look on the
model's Model Checking Results tab at the top of the
Distinct States column. As shown here, it shows
us that this version of
If there are few enough states, you may want the Toolbox to display the state graph TLC constructs. For that, you first have to download the Graphviz graph visualization program. You then have to tell the Toolbox where you put that program. Here's where to find out how to do that: Click Help on the Toolbox's top menu bar, then click on the Table of Contents option. Navigate as shown here to the help page for the TLC Options Page. On that page, click on Features and scroll down to Visualize state graph after completion and follow the instructions there for where to enter the location of the downloaded GraphViz program. (And after doing that, you might browse through the Toolbox's help pages to see what else is there.)
To tell TLC to produce the state graph, check the obvious option on the Features section of the model's TLC Options sub-tab. To raise that sub-tab, click on Additional TLC Options in the What to Check? section of the Model Overview sub-tab.
back to top