Re: [tlaplus] beginner's help with TLC

[Stephan Merz <stepha...@xxxxxxxxx>]

To follow up on Leslie's answer, here's what happens after you create a model from the SimpleAllocator specification (menu TLC Model Checker -> New Model...). The window will report two errors that correspond to the missing values for the CONSTANT parameters. A double click on the names of the constants in the tab named "What is the model?" will bring up a dialog box into which you enter the values. On the attached screenshot, I chose to instantiate the parameter Clients by the set {c1,c2,c3} and the parameter Resources by the set {r1,r2} and in both cases checked the box "set of model values" (meaning that TLC will consider them as uninterpreted, distinct constants), leaving all other options at their default values. Alternatively, I could have taken sets of pre-defined TLA+ values, say, integers or strings, and checked "Ordinary assignment".

It is somewhat confusing that the TLA+ Toolbox doesn't erase the error message once you assign values to these constants. Simply click on the triangle in the green circle at the top left of the interface. The interface then checks again, sees that everything is fine, and starts TLC.

Hope this helps. Best regards,

Stephan

On Saturday, March 9, 2013 3:43:12 AM UTC+1, Leslie Lamport wrote:

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.

 

Leslie

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...@googlegroups.com.
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.

Attachment: allocator.png
Description: PNG image