novice's troubles (continued)

[dmrl <dmrl...@xxxxxxxxx>]

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