Re: novice's troubles (continued)

[Leslie Lamport <tlapl...@xxxxxxxxx>]

Hi dmrl,

 

I could not see any attachments with your posting.  If you're having trouble with Google Groups, please send the attachments to my ordinary email address.   Along with those attachments, please also attach the log file in the subdirectory workspace/.metadata of the directory containing the Toolbox's executable.  Also, where did you get the two examples you tried? 

 

To answer your question, the cfg file is needed to run TLC from a command-line shell.  The Toolbox generates a new spec (which EXTENDS your spec) and a cfg file from the model and calls TLC on them.  This allows the Toolbox to implement many useful features, and frees you from having to deal with the inconvenience and limitations of the cfg file.

 

Leslie

 

On Tuesday, March 12, 2013 2:46:59 PM UTC-8, dmrl wrote:

Thanks much to Leslie and Stephan for the advice.
Sorry I was cryptic in my earlier post.

After realizing that the .cfg file does not work for TLC (BTW, what is then cfg's purpose?), I entered the model manually.  I tried the CarTalk and the SimpleAllocators examples.

The CarTalk tla file suggests how to use TLC to find the solution (attachment 1).
I am supposed to enter AllSolutions as the formula to be checked. On the model definition screen there is indeed an entry for "what to check" (attachment 2).  But that entry is disabled (greyed out).  Clicking it yields nothing.  And indeed running TLC on this model without further ado yields nothing (attachment 3).

Moving on to SimpleAllocator.tla, opening the tla file triggers a parsing error (attachment 4).  I have no idea where it comes from, because the file is verbatim the one posted online, and seems to be just fine.  Trying a few things leads nowhere, so I continue to enter the constants (attachment 5).  The error message is displayed in full in attachment 6. Trying TLC anyway gives a more forceful error message (attachment 7).

Any advice would be greatly appreciated.

-dmrl