# Advanced Options Page

    Contents
      Additional Definitions
      State Constraint
      Model Values
      Definition Override
      Action Constraint
      TLC Options

This model editor page allows you to add less-often used parts of a model. 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.

## 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 may be 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.

## TLC Options

You can choose between two basic ways of running TLC:

### Model-checking mode

This is the normal method of running TLC, in which it essentially tries to check all possible behaviors allowed by the behavior spec. Its default method of doing this is to find the graph of all reachable states using breadth-first search. This has the advantage that if TLC finds a violation of a safety property, then it will produce a shortest possible behavior that exhibits the error. You can direct TLC to use a depth-first search by choosing the Depth-first option and specifying the depth of its search. (Limiting the depth ensures that only a finite set of states is explored, even if the complete set of reachable states is infinite.) With depth-first search, TLC will usually not produce a shortest-length error trace. When running in depth-first mode, TLC does not compute the entire state graph and does not use a state queue, so it does not produce any Diameter or Queue size statistics.

Warning: Depth-first search is an experimental TLC option that has not been used much. We don't even know if it really works, let alone if it offers any advantages. If you do try it, let us know what you discover.

You can also specify a View to be used in model-checking mode. If you're curious about what that is and how it is used, see Section 14.3.3 (page 243) of Specifying Systems.

### Simulation Mode

In simulation mode, TLC does not try to examine all reachable states. Instead, it checks an unending series of behaviors, each of which it constructs by starting from a randomly choosen initial state and repeatedly making a random choice of a possible next state. (In this mode, you stop TLC by clicking the `Cancel` button on the dialog that the Toolbox pops up when it runs TLC.) You specify the maximum length of each behavior that it generates. If you want to know what specifying the Seed and Aril does, look them up in Specifying Systems. When run in simulation mode, the only statistics TLC reports are for States Found.

### Verify temporal properties upon termination only

Defer the verification of temporal properties (liveness) to the end of model checking. This reduces the overall model checking time with the additional side effect that invariant (safety) violations will always be found first. In other words, check liveness only after the complete state space has been checked for safety violations. If unchecked, temporal properties are checked periodically on the incomplete state graph. Defering verification of temporal properties is especially useful if it is highly likely that the model does not violate its temporal properties (e.g. a smaller instance of the model has successfully been verified for liveness violations).

### Fingerprint seed index

TLC saves only 64-bit fingerprints (hashes) of the reachable states that it finds, not the complete states. If two different reachable states have the same fingerprint, a situtation called a collision, TLC may not find all reachable states. At the end of a run, TLC prints estimates of how likely it was that a collision occurred. If you're worried that a collision might have occurred, you can re-run the model with a different fingerprint function. The fingerprint seed index specifies which of 64 fingerprint functions TLC should use. If the two runs produce different numbers of reachable states, then there was a collision in at least one of the runs. If not, the probability that there was a collision in both is the square of the probability that either one had a collision--a probability that is probably very, very small.

### Log base 2 of number of disk storage files

If your computer has multiple disk drives, setting this parameter to a value greater than 0 might make it possible to reduce the time TLC spends writing to disk on a model with a very large number of reachable states. Contact us for more information.

### Cardinality of largest enumerable set

If TLC tries to enumerate the elements of a set, it will report an error if the set contains more than this number of elements.

### Visualize state graph after completion of model checking

Visualize the generated state graph graphically after completion of model checking. The visualization helps to better understand the the system being specified. Initial states are represented by gray vertices.

Warning: Can reasonably only visualize small state graphs with a few dozen to hundred states.

In order to visualize a state graph, the path to the dot executable of the GraphViz project has to be set on the State Graph preference page on the File/Preferences menu. On macOS dot is most easily installed via the ports system. On Windows, can be obtained through Cygwin.

On Windows and Linux the state graph will be visualized with either the built-in or standalone PDF viewer depending on which is selected on the PDF viewer preference page (selecting the standalone viewer is advised for best results).

### JVM arguments

These are the arguments given to the Java Virtual Machine when TLC is run on the model. Certain parameters for running TLC in distributed mode are specified this way. Only sophisticated users who know what they are doing should specify other JVM arguments.

### TLC command line parameters

These are options given to TLC when it is run on the model. A complete list of TLC options can be found in the `tlatools > src > tlc2 > TLC.java` file in the CodePlex repository on the web. An option specified here can override an option otherwise specified by the rest of the model, which can cause strange things to happen. You should therefore use this feature with care. ↑ Creating a Model