Creating a Model

When you open a model, you open it in a model editor.  The model editor then shows only one page if the model has never been run before, and if it has been opened before, no other pages were kept open: — the Model Overview Page.
If the model has been run before, the Model Checking Results Page will be opened showing what the checker did the last time it was run.  The Model Overview Page contains links that open three other pages, the Spec Options page, the TLC Options page, and the Results / Constant Expressions page(s) should you want to work with Constant Expressions having not yet run the model a first time. You can switch between the pages using the tabs at the upper-left of the model editor view, or with the  Alt+PageUp  and  Alt+PageDown  keys.

You edit these pages in the usual way.  Sections can be opened or closed by clicking the  +  or  - . When entering text in fields, you can use your system's standard editing commands.

Whenever you enter a TLA+ expression as part of the model, that expression can use any symbols that you could use in a new definition placed at the end of the spec's root module.  It can also contain any model values that are declared in the model, as well as additional definitions entered in the Additional Definitions section of the Spec Options page.

Model Overview Page
Model Checking Results Page
Spec Options Page
TLC Options Page
↑ Model Checking