Contents Model description What is the behavior spec? What to check? What is the model? How to run?

This model editor page allows you to make the most common choices of the parameter values with which TLC is to be run. It contains links to the Spec Options Page for specifying additional options for telling TLC what spec behaviors to check and to the TLC Options Page for specifying additional ways to control the execution of TLC. Here are what the different sections of the Model Overview page are for.

**Init and Next**- A pair of formulas that specify the initial state and the next-state relation, respectively.
**Single formula**- A single temporal formula of the form
`Init /\ [][Next]`

, where_{vars}/\ F`Init`

is the initial predicate,`Next`

is the next-state relation,`vars`

is the tuple of variables, and`F`

is an optional fairness formula.

You can also choose to specify *No behavior spec*. This is the only option
if the spec has no variables. With this option, TLC will just check assumptions and
evaluate a constant expression, if you have entered one in the
*Evaluate Constant Expression* section
of the Model Checking Results Page.

**Ordinary assignment**- You can set the value of the constant to any constant TLA+ expression that
contains only symbols defined in the spec. The expression can even include
declared constants, as long as the value assigned to a constant does not depend
on that constant. (If there are circular dependencies, TLC will
produce a
`Java StackOverflowError`error.) **Model value**- It assigns to the constant a model value of the same name. (See
the
*Model Values and Symmetry*help page.) **Set of model values**- You must enter a comma-separated list of legal model-value names,
optionally enclosed by
`{`

and`}`

. You will have the option of making them a symmetry set.A

*typed*model value is one whose name begins with a letter and an underscore--for example,`p_42a`

. If you enter a set of model values that are not all of the same type, you will have to click`Next`to continue. You will then be given the choice of specifying a type for the set you have just entered. For example, if you entered the set`{2, a, b}`

and choose the type`t`

, the constant will be assigned the set`{t_2, t_a, t_b}`

of model values. Note that a number like`2`

is not a legal model value.See the

*Model Values and Symmetry*help page to learn about typed values and symmetry sets.

**Subtopics**- Model Values and Symmetry
- Running TLC in Distributed Mode