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.
If you want to use the same spec on different computers, see Keeping Copies of a Spec on Different Computers.
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 only one instance of the Toolbox at a time.