Re: [tlaplus] Scripting the Toolbox

I managed to the get it to work. Now I'm having a new problem. I have a project with 6 specifications arranged in a refinement sequence (actually, it might be more like a lattice).

When I launch the Toolkit IDE, I can model check all the specs and I get no errors. However, on the command line, I get the following:

localhost:Semaphore Simon$ java -classpath /Applications/toolbox/tla/ tlc2.TLC Sem0_Prog.tla

TLC2 Version 2.07 of 1 June 2015

Running in Model-Checking mode.

Parsing file Sem0_Prog.tla

Parsing file /Applications/toolbox/tla/tla2sany/StandardModules/Integers.tla

Parsing file /Applications/toolbox/tla/tla2sany/StandardModules/Sequences.tla

Parsing file /Applications/toolbox/tla/tla2sany/StandardModules/Naturals.tla

Parsing file Sem0_Spec.tla

Semantic processing of module Naturals

Semantic processing of module Integers

Semantic processing of module Sequences

Semantic processing of module Sem0_Spec

Semantic processing of module Sem0_Prog

Starting... (2016-04-16 12:37:39)

Error: TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.lang.RuntimeException: The constant parameter Pcs is not assigned a value by the configuration file.

Finished. (2016-04-16 12:37:39)

My directory structure is as following (considering only the files related to Sem0_Spec and the .tla and .cfg)

- Sem0_Prog.tla

- Sem0_Prog.cfg

- Sem0_Prog.toolbox

- Sem0_Prog.toolbox/Model_1

- Sem0_Prog.toolbox/Model_1/MC.cfg

- Sem0_Prog.toolbox/Model_1/MC.tla

- Sem0_Prog.toolbox/Model_1/Sem0_Prog.tla

I have tried the following combination of parameters:

java -classpath /Applications/toolbox/tla/ tlc2.TLC Sem0_Prog.tla

java -classpath /Applications/toolbox/tla/ tlc2.TLC Sem0_Prog/Model_1/Sem0_Prog.tla

java -classpath /Applications/toolbox/tla/ tlc2.TLC Sem0_Prog/Model_1/MC.tla

java -classpath /Applications/toolbox/tla/ tlc2.TLC -config Sem0_Prog/Model_1/MC.cfg Sem0_Prog.tla

java -classpath /Applications/toolbox/tla/ tlc2.TLC -config Sem0_Prog/Model_1/MC.cfg Sem0_Prog/Model_1/Sem0_Prog.tla

java -classpath /Applications/toolbox/tla/ tlc2.TLC -config Sem0_Prog/Model_1/MC.cfg Sem0_Prog/Model_1/MC.tla

java -classpath /Applications/toolbox/tla/ tlc2.TLC -config Sem0_Prog.cfg Sem0_Prog.tla

java -classpath /Applications/toolbox/tla/ tlc2.TLC -config Sem0_Prog.cfg Sem0_Prog/Model_1/Sem0_Prog.tla

java -classpath /Applications/toolbox/tla/ tlc2.TLC -config Sem0_Prog.cfg Sem0_Prog/Model_1/MC.tla

Am I doing something wrong?

I'm working with the version from June 2015.

On Saturday, April 16, 2016 at 11:14:14 AM UTC-4, Simon Hudon wrote:

Sorry, I hadn't seen that. Thanks!

Simon

On Saturday, April 16, 2016 at 10:37:26 AM UTC-4, Stephan Merz wrote:
Yes, of course. Please check out the documentation at http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html.

Regards,
Stephan

> On 16 Apr 2016, at 15:53, Simon Hudon <simo...@xxxxxxxxx> wrote:
>
> I would like to include my TLA+ specifications into my test suite. Is there a way of invoking the model checker from the command line?
>
> --
> 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 tlaplu...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.