Re: [tlaplus] Scripting the Toolbox

That's very good to know. How do you keep the cfg files in sync? I looked into MC.cfg under a Model_1/ directory and it doesn't seem self-contained as it references definitions from MC.tla. My goal would be to avoid getting different results when I invoke TLC from the command line and then from the toolbox.

On Sunday, April 17, 2016 at 10:04:31 AM UTC-4, Stephan Merz wrote:

As far as I know, the Toolbox cannot be directed to use user-provided .cfg files but manages its own .tla and .cfg files, in particular for displaying error messages. When I use the Toolbox in a shared project, I also keep the .toolbox/Model_x directories under version control.

Stephan

On 17 Apr 2016, at 15:56, Simon Hudon <simo...@xxxxxxxxx> wrote:

Ok, I see a bit better how to use the cfg files.

If I want to use both the command line and the toolbox in a project with a partner, is it sufficient to only have the version control track the .tla source file, the .cfg file but none of the files in the .toolbox directory? If so, how do I import that cfg file in the toolbox?

On Sunday, April 17, 2016 at 9:42:01 AM UTC-4, Simon Hudon wrote:
Thank you! I'll give it a read!

Simon

On Sunday, April 17, 2016 at 9:12:35 AM UTC-4, Stephan Merz wrote:
When using the command-line tools, the configuration files are provided by the user. The details are described in "Specifying Systems" (http://research.microsoft.com/en-us/um/people/lamport/tla/book.html), in particular Chapter 14. The Toolbox typically creates wrappers MC.tla and MC.cfg that extend the topmost TLA module provided by the user.

Stephan

On 17 Apr 2016, at 14:57, Simon Hudon <simon...@gmail.com> wrote:

Thank you! That sounds like a good idea. That's also what I try to do. The directories that I'm referring to above are created automatically by the toolbox when I create a specification.

At the root of my directory, here are the files that I have:
Sem0_Prog.tla
Sem0_Spec.tla
Sem1_Prog.tla
Sem1_Spec.tla
Sem2_Prog.tla
Sem2_Spec.tla
Sem0_Prog.cfg
Sem1_Prog.cfg
Sem2_Prog.cfg
The cfg files have been created by the toolbox and the curious thing is that they were only created for half of my TLA+ specs: the half that contains PlusCal algorithms. Do you ever have to create or modify those cfg files manually?

Thanks!
Simon

On Saturday, April 16, 2016 at 8:52:25 PM UTC-4, Leslie Lamport wrote:
A spec's root file, the .cfg file, and all imported modules other than standard modules should be in the same directory. I don't know if it's necessary, but I'd run TLC from that directory.

Leslie

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.