[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Scripting the Toolbox

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.


On 17 Apr 2016, at 14:57, Simon Hudon <simo...@xxxxxxxxx> 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?


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 tlaplu...@xxxxxxxxxxxxxxxx.
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.