You run the TLC model checker on a model of your spec. The model tells TLC what it should do. Here are the parts of the model that you must explicitly choose:
The Model Overview, Spec Options, and TLC Options help pages describe all the things that can go into a model.
A specification may contain multiple models. You can create a new model, open an existing one, or create a clone (a copy with a new name) of an existing model by clicking on the TLC Model Checker menu. Alternatively, you can use the Spec Explorer. To create a new model, open the Spec Explorer and right-click on the currently open spec. To open an existing model, open the spec's menu item (by clicking on the + ) and double-clicking on the model. Right-clicking on the model also gives you the options of renaming it, deleting it, and creating a clone.
A convenient way to examine all the spec's models
is by selecting Quick Access on the Window menu
or typing Control+Shift+A. This raises a window showing the models
and the beginning of their Model Description fields. Double-clicking
on a model opens it.
You can also open
imported modules from that window. Check out the window's options menu.
When you model check a spec, you should begin with a very small model--that is, a model for which the values substituted for constants (and perhaps a constraint) yield a small set of reachable states. Before you've model checked it, your spec almost surely contains quite a few errors. Using a small model, TLC can find the trivial ones very quickly. When it finds no errors in a small model, you can then gradually increase the size of the model.
As you run your spec on larger and larger models, it's easy to forget what you've done. Instead of changing a model and running it again, create a new model and keep the old one. (This is easy to do by cloning the model, as described above.) You can identify your models with the Model Description field, which is shown It will be easier to identify your models if you put the important contents of the model in the model name--for example, you can name a model
N=3,Proc={a1,a2,a3}
The model is always locked while it is being run by TLC. This means that
you can't view information in sections of a running model that are closed.
It's therefore a good idea to open all sections of the model
that you might want to look at before starting a TLC run that will
take a significant amount of time.
If you forget to do this, you can clone the running model and examine
the clone.
The Toolbox saves a copy of the version of the spec on which the model was run or checked, so you can look at it even after you have changed the spec. You can examine any modules in the saved version by clicking on the Open Saved Module command on the TLC Model Checker menu when the model is selected. (The model is selected when one of its pages has the focus.) The How TLC is Run help-page section tells you where those saved modules are saved.