When you open a model, you open it in a model editor. The model editor has three pages: The Model Overview Page and Advanced Options Page specify the model. The Model Checking Results Page shows you either what the model checker is doing while it runs, or what it did the last time it was run. 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 Advanced Options Page.
A model can be locked or unlocked by using the lock icon or the key icon in the upper-left part of each model-editor page. The model is always locked while it is being run by TLC, and it remains locked after TLC completes unless the run was short.