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