A clarification: For a spec S, the Toolbox creates a directory S.toolbox. That directory contains a subdirectory for each TLC model. The Toolbox creates a file MC.tla in that subdirectory and runs TLC on the model by executing it on that file. The Toolbox's "check model" command, executed by clicking on the icon with two gears and two arrows, creates the file without running TLC. You can run TLC directly on that file from outside the Toolbox.
Leslie
On Thursday, March 1, 2018 at 11:33:12 AM UTC-8, Stephan Merz wrote:
Hello,
the values allowed in configuration files are indeed quite limited (see “Specifying Systems” for the precise syntax). You need to define a constant in the TLA specification, e.g.
MyTuple == << 1,2,3 >>
and then assign MyTuple to the constant. The Toolbox does the same for you behind the scenes, look at the module MC.tla in the toolbox directory created for your specification.
Regards,
Stephan