Re: [tlaplus] Scripting the Toolbox

[Leslie Lamport <tlapl...@xxxxxxxxx>]

As Stephan explained, the Toolbox runs TLC on the MC spec (using
MC.cfg) in the model's directory, which is a subdirectory of the
spec's .toolbox directory.  Running TLC from the command line on that
spec in that directory will produce the same results as running TLC on
the model from the Toolbox--if TLC is run with the same parameters.
Note that the Toolbox runs TLC with the -tool parameter, which is
probably not what you want it to do when running it from the command
line.

Markus informs me that the Toolbox stores the definition of a model in
the model's .launch file.  The model's directory contains the .tla and
.cfg files on which the model was last run.  That subdirectory is
re-created by the run model and check model commands.

As I believe is explained in the help pages, the .launch file contains
complete path names of the relevant files.  So if those files are
shared between users, you will have to make sure that the specs are
kept in folders with the same path names, or else those files have to
be edited after they are copied.  Also, if a Toolbox file is changed
from outside the Toolbox, the Toolbox may complain.  In that case, it
is necessary to execute the refresh spec command from the Spec
Explorer window.  We're sorry about this, but the Eclipse infrastructure
used by the Toolbox apparently makes it a lot of work to do backup and
sharing of models right.