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:

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