Spec Options Page

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.

Additional Definitions

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.

State Constraint

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.

Model Values

You can enter here a set of model values, which you can then use in expressions that define the model--for example, in the value substituted for a declared constant.  See the Model Values and Symmetry help page for an explanation of what model values are and how they are used.

Definition Override

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.

Action Constraint

An action constraint is much like a state constraint, except that the constraint formula may also include primed variables.  See Section 14.3 (page 240) of Specifying Systems for an explanation of how TLC uses an action constraint.
↑ Creating a Model