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.