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
.
.tla
) and the specification name.
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.
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.
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.