You don't use a cfg file when running TLC from the Toolbox. On the Toolbox, go to Help > Dynamic Help > Contents > Model Checking.to find out how to run TLC. You will have to enter in the Toolbox the information that you put in your cfg file, but doing so is quite easy.
On Fri, Mar 8, 2013 at 5:41 PM, dmrl
<lei...@xxxxxxxxxxx> wrote:
I am a novice to TLA+, which I try to incorporate into a course I teach.
I'd appreciate advice on the following difficulty, even if (and particularly if) it is laughably naive.
Running TLC from the toolbox calls for a cfg file, right?
I am trying to run TLC for the TLA+ examples copied over verbatim from the TLA+ site (SimpleAllocator, Prisoners, CarTalkPuzzle...).
I uniformly get an error message from the parser, asking for the values of constants, which are already given in the cfg file. I try to entre them manually anyway, using the same format as in the cfg file, as well as all the variants I can think of. I still get the same error messages.
thnx for any and all advice - dmrl
--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.