Scripting the Toolbox

[Simon Hudon]

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?

[Stephan Merz]

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 <simon...@gmail.com> 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 tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Simon Hudon]

Sorry, I hadn't seen that. Thanks!

Simon

[Simon Hudon]

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.

[Leslie Lamport]

A spec's root file, the .cfg file, and all imported modules other than standard modules should be in the same directory.  I don't know if it's necessary, but I'd run TLC from that directory.

Leslie

[Simon Hudon]

Thank you! That sounds like a good idea. That's also what I try to do. The directories that I'm referring to above are created automatically by the toolbox when I create a specification.

At the root of my directory, here are the files that I have:

• Sem0_Prog.tla
  
• Sem0_Spec.tla
  
• Sem1_Prog.tla
  
• Sem1_Spec.tla
  
• Sem2_Prog.tla
  
• Sem2_Spec.tla
  
• Sem0_Prog.cfg
  
• Sem1_Prog.cfg
  
• Sem2_Prog.cfg
  

The cfg files have been created by the toolbox and the curious thing is that they were only created for half of my TLA+ specs: the half that contains PlusCal algorithms. Do you ever have to create or modify those cfg files manually?

Thanks!

Simon

[Stephan Merz]

When using the command-line tools, the configuration files are provided by the user. The details are described in "Specifying Systems" (http://research.microsoft.com/en-us/um/people/lamport/tla/book.html), in particular Chapter 14. The Toolbox typically creates wrappers MC.tla and MC.cfg that extend the topmost TLA module provided by the user.

Stephan

[Simon Hudon]

Thank you! I'll give it a read!

Simon

[Simon Hudon]

Ok, I see a bit better how to use the cfg files. 

If I want to use both the command line and the toolbox in a project with a partner, is it sufficient to only have the version control track the .tla source file, the .cfg file but none of the files in the .toolbox directory? If so, how do I import that cfg file in the toolbox?

Simon

[Stephan Merz]

As far as I know, the Toolbox cannot be directed to use user-provided .cfg files but manages its own .tla and .cfg files, in particular for displaying error messages. When I use the Toolbox in a shared project, I also keep the .toolbox/Model_x directories under version control.

Stephan

On 17 Apr 2016, at 15:56, Simon Hudon <simon...@gmail.com> wrote:

Ok, I see a bit better how to use the cfg files. 

If I want to use both the command line and the toolbox in a project with a partner, is it sufficient to only have the version control track the .tla source file, the .cfg file but none of the files in the .toolbox directory? If so, how do I import that cfg file in the toolbox?

[Simon Hudon]

That's very good to know. How do you keep the cfg files in sync? I looked into MC.cfg under a Model_1/ directory and it doesn't seem self-contained as it references definitions from MC.tla. My goal would be to avoid getting different results when I invoke TLC from the command line and then from the toolbox.

[Leslie Lamport]

As Stephan explained, the Toolbox runs TLC on the MC spec (using
MC.cfg) in the model's directory, which is a subdirectory of the
spec's .toolbox directory.  Running TLC from the command line on that
spec in that directory will produce the same results as running TLC on
the model from the Toolbox--if TLC is run with the same parameters.
Note that the Toolbox runs TLC with the -tool parameter, which is
probably not what you want it to do when running it from the command
line.

Markus informs me that the Toolbox stores the definition of a model in
the model's .launch file.  The model's directory contains the .tla and
.cfg files on which the model was last run.  That subdirectory is
re-created by the run model and check model commands.

As I believe is explained in the help pages, the .launch file contains
complete path names of the relevant files.  So if those files are
shared between users, you will have to make sure that the specs are
kept in folders with the same path names, or else those files have to
be edited after they are copied.  Also, if a Toolbox file is changed
from outside the Toolbox, the Toolbox may complain.  In that case, it
is necessary to execute the refresh spec command from the Spec
Explorer window.  We're sorry about this, but the Eclipse infrastructure
used by the Toolbox apparently makes it a lot of work to do backup and
sharing of models right.

[Markus Alexander Kuppe]

On 18.04.2016 18:59, Leslie Lamport wrote:
> As I believe is explained in the help pages, the .launch file contains
> complete path names of the relevant files. So if those files are
> shared between users, you will have to make sure that the specs are
> kept in folders with the same path names, or else those files have to
> be edited after they are copied.

Hi,

starting with version 1.5.1 of the Toolbox (May 2015), none of the files
should contain absolute path names anymore.

Cheers
Markus