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

You can create a new spec with the  File/Open Spec/Add New Spec...  menu item.  It raises a dialog asking you to choose the root file (which must have the extension .tla) and the specification name.

Open

You can open an existing spec by choosing it from the  File/Open Spec menu.   You can also use the Spec Explorer, 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 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.  When you modify the spec or its models on one machine, just copy the module files and .toolbox directory to the other machine.  Strange things can happen if a spec's files (its modules or the files in its .toolbox directory) have changed since the last time the Toolbox read or wrote them.  It's therefore a good idea to close the Toolbox before copying a new version of a spec from another machine.  If a spec's files do change while the Toolbox is open, it's a good idea to right-click on the spec in the Spec Explorer and execute the Refresh command.  If strangeness still occurs, try closing and re-opening the Toolbox.  If that doesn't fix the problem, see Getting Out of Trouble.


↑ Managing Your Specifications