parsing config file in command line mode

[Kirsten Winter]

Dear Colleagues,

I want to run TLC from a command line and get
the following parsing error:

TLC2 Version 2.08 of 21 December 2015
Running in Model-Checking mode.
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 tlc2.tool.ConfigFileException
: TLC found an error in the configuration file at line 7
It was expecting = or <-, but did not find it.
Finished in 00s at (2017-02-10 10:12:23)

using the following configuration file:

CONSTANT
null = 0
N = 3
T = {1,2}
Ref = {1,2,3}
empty = 0
undef = <<3,3>>

SPECIFICATION
Spec

INVARIANTS
ABS
INV
STATUS

If I use the value <<3,3>> directly in the module (instead of using the
constant "undef") the parser
is happy.

The corresponding module file as well as the configuration file are
attached.

Thank you for your help,
Kirsten

[Leslie Lamport]

TLC allows only a restricted class of expressions in a configuration file.  See "Specifying Systems" for the exact syntax.  Why aren't you running TLC from the Toolbox?

Leslie

[Kirsten Winter]

Thanks for your quick reply, Leslie.

In a student project last year our student extended the toolbox to build a "Linearisability checker"
using TLC as a backend. As a frontend she modified the toolbox code which worked fine.
The student has left now and we are not able to rebuild the toolbox with her modified
code. This could be due to changes in the toolbox or our lack of knowledge of how to
integrate code into maven. Hence we are stuck and contemplating to build our own
frontend from scratch.

For the time being we want to run  some experiments in batch mode.

Kirsten

[Stephan Merz]

Hi Kirsten,

in order to get around the restrictions on expressions allowed in configuration files, you may consider doing like the Toolbox does when it calls TLC: create an intermediate TLA+ module that extends the original one and adds extra definitions corresponding to the values to be substituted for constant parameters. In your case, something like

@null == 0

@N = 3

...

@undef = <<3,3>>

Then create a configuration file for that new module where the constants from the original module are replaced by the constants defined in the intermediate module, like so

null <- @null

N <- @N

...

undef <- @undef

(plus any model values). In this way, your configuration file never contains complex expressions.

Stephan