Contents Additional Definitions State Constraint Model Values Definition Override Action Constraint TLC Options
This model editor page allows you to add less-often used parts of a model. It's a good idea to browse this page just to see what options it provides, since some of the features are not ones you would expect.
It is sometimes convenient to define operators just for use in the expressions that specify a model. For example, you might want to define an operator that you use can use in more than one invariant. If you don't want those definitions to be part of the spec, you can put them in this section of the page. These definitions can use any operator or parameters that can be used in the the root module, as well as any model value that is declared in the model.
In addition to definitions, in this section you can also
put assumptions (ASSUME statements)
for TLC to check. Putting other
things in this section, such as declarations,
will result in mysterious TLC errors.
Many behavior specifications have an infinite set of reachable states. For example, message queues could get arbitrarily large. TLC will run forever (or until your computer runs out of disk space) on such a behavior spec. You could just let it run and keep looking for violations of safety properties such as invariance. However, it's a better idea to limit the set of states by entering a state constraint here.
A state constraint is a state predicate, which is a
Boolean-valued expression that contains unprimed variables.
When computing the set of reachable states, TLC will not
explore successor states of any state it finds that does
not satisfy the state constraint. For example,
specifying len < 3 essentially
limits the set of reachable states that TLC finds to ones
that can be reached by a sequence of states in which
the value of the variable len
is less than 3. See Section 14.3 (page 240) of
Specifying Systems for an explanation of how TLC
computes reachable states. Note that there is no need
for multiple state constraints because they can simply be
conjoined to form a single constraint.
We want our specifications to be as simple and easy to understand as possible. Sometimes this leads to a definition that TLC cannot evaluate, or that it can evaluate only very inefficiently. In that case, we must override the definition by telling TLC to replace it with a new definition. To do this, click on the section's Add button, select the operator whose definition you want to override, and click OK . (You can also double-click on the operator name.) This will raise a dialog in which you can specify the overriding.
If the operator whose definition you are overriding has arguments, you will be presented with a form for writing the new definition in the obvious way. If it has no arguments, you have two options. With the Ordinary assignment option, you just write the new definition. The Model value option defines the operator to equal a model value of the same name. See the Model Values and Symmetry help page for an explanation of model values and the most common reason why you would want to override the definition in this way.
You can override definitions made in modules other than the root module. If a definition is in a module imported with an INSTANCE statement, then the name of the module may be indicated.
You can edit or remove an overriding specification in the obvious way: by selecting it and using the Edit or Remove button. (Editing is also selected by double-clicking on the item.)
Some Fine Print
When overriding a definition,
the new definition can use any operator or parameters that
can be used in the the root module, as well as any
model value that is
declared in the model. This means that you can override
a definition with an expression that
contains operators that are undefined at the point where the
original definition occurred.
TLC evaluates overridden definitions in the
obvious way, and bizarre overriding can
lead to strange results. For example, if Fact is defined by
Fact(n) == IF n = 0 THEN 1 ELSE n * Bar(n-1)
and the definition of Bar is overridden with
Bar(n) <- Fact(n)
then TLC will evaluate Fact(n) to
equal n! for any natural
number n .
There is no good reason to use such bizarre overriding.
This is the normal method of running TLC, in which it essentially tries to check all possible behaviors allowed by the behavior spec. Its default method of doing this is to find the graph of all reachable states using breadth-first search. This has the advantage that if TLC finds a violation of a safety property, then it will produce a shortest possible behavior that exhibits the error. You can direct TLC to use a depth-first search by choosing the Depth-first option and specifying the depth of its search. (Limiting the depth ensures that only a finite set of states is explored, even if the complete set of reachable states is infinite.) With depth-first search, TLC will usually not produce a shortest-length error trace. When running in depth-first mode, TLC does not compute the entire state graph and does not use a state queue, so it does not produce any Diameter or Queue size statistics.
Warning: Depth-first search is an experimental TLC option that has not been used much. We don't even know if it really works, let alone if it offers any advantages. If you do try it, let us know what you discover.
You can also specify a View to be used in model-checking mode. If you're curious about what that is and how it is used, see Section 14.3.3 (page 243) of Specifying Systems.
In simulation mode, TLC does not try to examine all reachable states. Instead, it checks an unending series of behaviors, each of which it constructs by starting from a randomly choosen initial state and repeatedly making a random choice of a possible next state. (In this mode, you stop TLC by clicking the Cancel button on the dialog that the Toolbox pops up when it runs TLC.) You specify the maximum length of each behavior that it generates. If you want to know what specifying the Seed and Aril does, look them up in Specifying Systems. When run in simulation mode, the only statistics TLC reports are for States Found.
Defer the verification of temporal properties (liveness) to the end of model checking. This reduces the overall model checking time with the additional side effect that invariant (safety) violations will always be found first. In other words, check liveness only after the complete state space has been checked for safety violations. If unchecked, temporal properties are checked periodically on the incomplete state graph. Defering verification of temporal properties is especially useful if it is highly likely that the model does not violate its temporal properties (e.g. a smaller instance of the model has successfully been verified for liveness violations).
TLC saves only 64-bit fingerprints (hashes) of the reachable states that it finds, not the complete states. If two different reachable states have the same fingerprint, a situtation called a collision, TLC may not find all reachable states. At the end of a run, TLC prints estimates of how likely it was that a collision occurred. If you're worried that a collision might have occurred, you can re-run the model with a different fingerprint function. The fingerprint seed index specifies which of 64 fingerprint functions TLC should use. If the two runs produce different numbers of reachable states, then there was a collision in at least one of the runs. If not, the probability that there was a collision in both is the square of the probability that either one had a collision--a probability that is probably very, very small.
Visualize the generated state graph graphically after completion of model checking. The visualization helps to better understand the the system being specified. Initial states are represented by gray vertices.
Warning: Can reasonably only visualize small state graphs with a few dozen to hundred states.
In order to visualize a state graph, the path to the dot executable of the GraphViz project has to be set on the State Graph preference page on the File/Preferences menu. On macOS dot is most easily installed via the ports system. On Windows, can be obtained through Cygwin.
On Windows and Linux the state graph will be visualized with either the built-in or standalone PDF viewer depending on which is selected on the PDF viewer preference page (selecting the standalone viewer is advised for best results).
tlatools > src > tlc2 > TLC.java
file in the
CodePlex repository on
the web.
An option specified here can override an option otherwise specified by the rest of the model,
which can cause strange things to happen. You should therefore use this
feature with care.
↑ Creating a Model