Contents Additional Definitions State Constraint Model Values Definition Override Action Constraint
This model editor page allows you to add less-often used parts of a model that describe the spec that the Toolbox calls TLC to check. 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. The page is raised from a link on the Model Overview Page.
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 containing the definition is 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.