# Model Overview Page

    Contents
      Model description
      What is the behavior spec?
      What to check?
      What is the model?
      How to run?
      Running in Distributed Mode

This model editor page is usually the only one you will use to create and run your model. Here are what the different sections of the page are for.

## Model description

Enter any text you want here. The first line of the text is displayed in the Quick Access window's list of models.

## What is the behavior spec?

The behavior spec is the formula or pair of formulas that describe the possible behaviors of the system or algorithm you want to check. (See the What Is A Spec? help page.) There are two ways to write the behavior spec:

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]vars /\ F`, where `Init` is the initial predicate, `Next` is the next-state relation, `vars` is the tuple of variables, and `F` is an optional fairness formula.

The only way to write a behavior spec that includes fairness is with a temporal 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.

## What to check?

There are three kinds of properties of the behavior spec that TLC can check:

### Deadlock

A deadlock is said to occur in a state for which the next-state relation allows no successor states. Termination is deadlock that is not considered an error. If you want the behavior spec to allow termination, then you should uncheck the deadlock option. (This is not necessary for the spec produced by translating a PlusCal algorithm, because its next-state relation is written in a way that causes TLC not to consider normal termination to be a deadlock.)

### Invariants

An invariant is a state predicate that is true of all reachable states--that is, states that can occur in a behavior allowed by the behavior spec. You can include a list of invariants. The checking of each invariant can be enabled or disabled by checking or unchecking its box.

### Properties

TLC can check if the behavior spec satisfies (implies) a temporal property, which is expressed as a temporal-logic formula. You can specify a list of such properties, each with a check-box for enabling or disabling its checking.

## What is the model?

The most basic part of a model is an assignment of values to declared constants. To assign a value to a constant, either double-click on the constant or select it and click on the `Edit` button. This will raise a pop-up dialog giving you the choice of three ways to assign a value to it:

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

## How to run?

Here, you specify the following two aspects of how TLC should be run. (See the TLC Options section of the Advanced Options Page help page for additional ways to run TLC.)

### TLC Parameters

There are two parameters that you can set here:

#### Number of worker threads

TLC's algorithm for computing the set (actually the graph) of reachable states is highly parallelizable, and it can make good use of arbitrarily many processors. This parameter specifies the number of separate threads that TLC will spawn to perform that computation. You should not set it to be greater than the number of separate processors (cores) on your computer; the Toolbox will warn you if you do.

#### Fraction of physical memory allocated to TLC

This determines how large a heap TLC will use. If you make it too small, TLC could run out of heap space and crash. If you make it too large, your machine will not have enough memory and everything will run slowly. The slider's color warns you if you are giving TLC too little or too much memory. TLC can keep the set of reachable states it has found on disk, so having too many reachable states can't run it out of memory. However, it runs much faster when it can keep those states in memory. TLC can run out of heap space if it takes too much memory to represent the set of initial states or the set of successor states of a single state. If TLC does run out of memory in the middle of a long run, you can give it more and restart it from a checkpoint.

Setting the this parameter too large may produce a Could not create the Java virtual machine error.

### Checkpoint Recovery

TLC takes regular checkpoints, from which it can be restarted if it is stopped for any reason--for example, if your computer crashes. The Recover from checkpoint option tells TLC to start from where it was when the last checkpoint was taken. This option is enabled if the last time you ran TLC, it ran long enough to produce a checkpoint. The Toolbox will fill in the Checkpoint id for you.

Warning: If you exit the Toolbox, it will stop any executions of TLC that are in process. However, it is possible to stop the Toolbox in some drastic fashion that leaves TLC running as a background process. Restarting from a checkpoint while the TLC process that created it is still running can cause the checkpoint to be destroyed, making recovery impossible. If you have reason to believe TLC was not stopped, check to see if it is still running before trying to recover from a checkpoint.

The checkpoint TLC produces after a short run does not take up much space. However, if TLC finds an error after running for a long time, the checkpoint files could take up a lot of space--sometimes on the order of a gigabyte for a model that has run for several days. These files are deleted if the model is re-run and a new checkpoint is produced, or if the model is validated when the Recover from checkpoint option is not selected. When TLC has created a checkpoint, the How to Run section of the Model Overview page displays how much storage the checkpoint occupies. It also provides a button that you can click to delete the checkpoint.

Checkpointing does not yet work when TLC is run in distributed mode.

### Running in Distributed Mode

TLC can be run with worker threads run on multiple machine, considerably speeding up its execution. See Running TLC in Distributed Mode

Subtopics
  Model Values and Symmetry
  Running TLC in Distributed Mode

↑ Creating a Model