Managing Your Specifications

If you are using the Toolbox, you should have some knowledge of the TLA+ specification language.  (See the TLA+ Resources help page for information on how to acquire this knowledge.).  You should therefore have a basic understanding of what a TLA+ specification is.  We usually use the term spec instead of specification.

The Toolbox allows you to create, edit, and check one spec at a time.  See the subtopics listed below to find out how to create, modify, view, and parse your spec. 

Running the TLC Model Checker on a spec can sometimes create a lot of data associated with the spec.  See the TLA+ Preferences help page to learn how to find out how much storage your spec is using and what to do if it is using too much.

You may want to use the same modules in different specs--for example, ones that define data structures that you want to re-use.  The best way to do that is to put those modules in one or more library folders. See the TLA+ Preferences help page.

You can run multiple instances of the Toolbox to work on different specifications concurrently.  Do not open the same specification in two different instances of the Toolbox at the same time.


Subtopics
What is a Spec?
Manipulating Specs
Parsing
Editing Modules
Pretty-Printing Modules
↑ TLA+ Toolbox User's Guide