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 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.