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