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