# Model Values and Symmetry

    Contents
      Ordinary Model Values
      Typed Model Values
      Using Model Values
      Symmetry

## Ordinary Model Values

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 Nat

It 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 Advanced 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 Advanced Options Page and then use them as ordinary values in expressions of the model.

## Typed Model Values

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_` .

## Using Model Values

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 Advanced Options Page, by choosing the Model value option.
- In the Model Values section of the Advanced Options Page.

## Symmetry

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.

↑ Model Overview Page