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:

- When assigning a value to a constant parameter in the
What is the model? section of
the
*Model Overview Page*, by choosing the*Model value*or*Set of model values*option. - When overriding a definition in the Definition override
section of the
*Spec Options Page*, by choosing the*Model value*option. -
In the Model Values section of the
*Spec Options Page*.

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} : TRUEis 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.**

↑ Model Overview Page