Manipulating Specs

A specification has a name and a root module, which is in a file whose extension is .tla.  You will probably give your spec the same name as its root module, but you need not.  Two different specs cannot have the same name.  Here are the Toolbox's spec operations.

Warning: if you want to use the model checker, your spec must not contain a module named  MC .

Create

Open

, which is opened either from the File menu or by clicking on the icon on the left side of the Toolbox, near the top.  Right-click on the desired spec and select Open.   If you open a spec when another spec is open, the other spec will automatically be closed.

Close

You can close a spec with the  File/Close Spec  menu.  This returns you to the Welcome View.    However, remember that the Toolbox will close the current spec if you open another one.

Rename, Forget, and Delete

Forgetting a spec means that the Toolbox removes it from the Spec Explorer and the list of specs presented by the File/Open Spec menu.  If you later re-open a spec with the same name in the same folder, then you will be able to import to previous spec's models.  Deleting a spec means forgetting it and deleting its models, but not any of its modules.  Renaming a spec changes the spec's name, but not the name of its root module.  You can rename, forget, or delete or rename an existing spec by opening the Spec Explorer (described above), right-clicking on the desired spec, and making the appropriate choice. 

Note: here's how to change the name of both a spec and its root module from Foo to Bar: Rename spec Foo to Bar, save module Foo as module Bar (using the File/Save As command), Forget module Bar, and Open a new spec named Bar with module Bar as its root module. 

Finding Your Spec

It's easy to forget where in your file system a spec's module files are.  A file's complete path name should appear at the top of the editor window.  You can also find the root-module file's complete path name by opening the Spec Explorer view, right-clicking on the spec's name, and selecting  Properties .   (The rest of the spec's module files are in the same folder.)

Moving a Spec from Elsewhere

Here is how to move an existing spec named  SName to a different folder (directory) on the same computer, or to a different computer.   Copy all the spec's module files (the root-module file and its imported module files) and the folder (directory) named  SName.toolbox  to the new location.   (If you're using TLAPS, also copy the directory SName.tlaps.)  

If there is already a spec named SName (which will be the case if you're moving the spec to a different place on the same computer), have the Toolbox forget or delete it.   Open a new specification named SName using the new copy of the root-module file.

Keeping Copies of a Spec on Different Computers

You may want to run the Toolbox on different machines for the same spec.  Once you've created a spec on one machine, copy the spec's module files and .toolbox directory to the other machine and use the instructions above to create a copy of the spec on that machine.  The Toolbox can get confused if a spec or its models is modified from from outside the Toolbox.  So, here's how to import changes to a spec or its models from another computer onto the computer you're now using.

1. If the spec is open in the Toolbox, close it.
2. Move the spec's module files, its .toolbox directory, and its .tlaps directory (if you're using TLAPS) onto the current machine. 
3. Open the Toolbox's Spec Explorer, right-click on the spec, and execute the Refresh command.

If you forget to close the spec before externally modifying its files, closing the spec and refreshing it may solve the problem.  If it doesn't, see Getting Out of Trouble.