Contents Ordinary Model Values Typed Model Values Using Model Values Symmetry
A model must specify the values of all declared constants.
You will sometimes want to let a constant equal an unspecified value or a finite
set of unspecified values. For example, the spec might have a
constant Proc whose value
represents a set of processes.
You could just let a process be a number, substituting an ordinary value
like {1, 2, 3}
for Proc . However, a better way is to represent a process by a TLC
model value. A model value is an unspecified value
that TLC considers to be unequal to any value that you can express
in TLA+. You can substitute the
set {p1, p2, p3} of three model values
for Proc . If by mistake you write an expression
like p+1 where the value of p is
a process, TLC will report an error when it tries to evaluate that expression
because it knows that a process is a model value and thus not a number.
An important reason for
substituting a set of model values for Proc is
to let TLC take advantage of symmetry, as described below.
There is one particular TLA+ specification idiom that requires you to substitute a model value for a defined operator. Here is a typical example of this idiom.
NotANat == CHOOSE n : n \notin NatIt defines
NotANat to be an arbitrary value
that is not a natural number. TLC cannot evaluate this definition because
it cannot evaluate the unbounded CHOOSE expression.
To allow TLC to handle the spec, you need to substitute a model value
for NotANat . The best model value to substitute for it
is one named NotANat . This is done in the
Definition Override section of
the Spec Options Page. The Toolbox will
create the appropriate entry in that section when it creates a model
if it finds a definition having the precise
syntax above or the syntax
NotANat == CHOOSE n : ~(n \in Nat)where
Nat can be any expression, and NotANat and n
can be any identifiers.
There are some uses of model values that can't be specified with the What is the model? section of the Model Overview Page. If you encounter such a problem, you can declare your own set of model values with the Additional Definitions section of the Spec Options Page and then use them as ordinary values in expressions of the model.
Suppose that, by mistake, you write the
expression p=2 where p is
a process. If you substitute a set of ordinary model values for the set
of processes, TLC will simply obtain the value FALSE
if it evalutes this expression, since it considers an ordinary model value
to be different from any other value. To allow TLC to detect this kind of error,
you can use a set of typed model values. TLC considers a typed model value
to be unequal to any other model value of the same type. However, it produces an
error when evaluating an expression requires it to determine if a typed model value
is equal to any value other than a model value of the same type or an ordinary model value.
A model-value type consists of
a single letter, so there are 52 different types because a
and A are different types.
(TLC actually accepts digits and underscore as types; don't use them.)
A model value has
type T if and only if its name begins with the two
characters T_ .
A model value declared in the model can be used as an ordinary value in any expression that
is part of the model's specification. For example, suppose your spec has a
constant Proc that represents a set of processes
and a constant Leader that is some element
of Proc . You can substitute the
set {p1, p2, p3} of model values
for Proc using the Set of model values
option of the What is the model?
section of the Model Overview Page. You
can then
substitute p1
for Leader using the Ordinary assignment
option of that section.
Model values can be declared in the following places:
Consider a specification of a memory system containing a declared
constant Val that represents the set of
possible values of a memory register. The set Val of values is probably a
symmetry set for the memory system's behavior specification,
meaning that permuting
the elements in the set of values does not change whether or not
a behavior satisfies that behavior spec. TLC can
take advantage of this to speed up its checking.
Suppose we substitute a
set {v1, v2, v3} of model values
for Val . We can use
the
Symmetry set
option of the What is the model?
section of the Model Overview Page
to declare this set of model values to be a symmetry set of the behavior spec.
This will reduce the number of reachable states that TLC has to examine
by up to 3!, or 6.
You can declare more than one set of model values to be a symmetry set. However, the union of all the symmetry sets cannot contain two typed model values with different types.
TLC does not check if a set you declare to be a symmetry set really
is one. If you declare a set to be a symmetry set and it isn't, then
TLC can fail to find an error
that it otherwise would find.
An expression is symmetric for a set S if and only if
interchanging any two values of S does not
change the value of the expression. The expression
{{v1, v2}, {v1, v3}, {v2, v3}}
is symmetric for the set
{v1, v2, v3} --
for example, interchanging v1 and v3
in this expression produces
{{v3, v2}, {v3, v1}, {v2, v1}},
which is equal to the original expression.
You should declare a set S of model values to be a symmetry set only if
the specification and all properties you are checking are symmetric for S
after the substitutions for constants and defined operators specified by the model
are made.
For example, you should not declare
{v1, v2, v3}
to be a symmetry set if the model substitutes v1 for some constant.
The only TLA+ operator that can produce a non-symmetric expression when applied to
a symmetric expression is CHOOSE. For example, the expression
CHOOSE x \in {v1, v2, v3} : TRUE
is not symmetric for {v1, v2, v3}.
Symmetry sets should not be used when checking liveness properties. Doing so can make TLC fail to find errors, or to report nonexistent errors.