[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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.
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!
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.
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:
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?
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.
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.