Re: [tlaplus] novice's troubles (continued)

With the CarTalk example, dmrl was confused by the confusing overloading of the term "spec". The usual TLA spec is a temporal formula. A temporal formula is a predicate on behaviors, where a behavior is a sequence of states and a state is an assignment of values to variables. This is the kind of spec that you have to use to describe a concurrent system. To distinguish it from other kinds of specs, I now call it a "behavior spec". The "What to Check?" part of the model is in the section "What is the behavior spec?". As dmrl reported, the model indicated that there is no behavior spec, which is why "What to Check?" was greyed out. The Toolbox knew that there couldn't be a behavioral spec because there were no variables declared in the module.

The spec in the CarTalk example is the _expression_ AllSolutions. It is a constant _expression_. When you expand all the definitions, the only things that mathematicians call "variables" in the _expression_ are the declared TLA constants N and P. (In TLA, constants are what temporal logicians call rigid variables; TLA's variables are what they call flexible variables.) To have TLC evaluate a constant _expression_ for a model (which must define values for declared constants), you must go to the model's Model Checking Results page. In the section "Evaluate Constant _expression_", type the _expression_ you want TLC to evaluate in the text field marked "_expression_:" and click on the Run button (the button with the arrowhead in the green circle). TLC should print the value in the obvious place.

-----------------------

On Tue, Mar 12, 2013 at 2:46 PM, dmrl <dmrl...@xxxxxxxxx> 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

--
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.