Re: parsing config file in command line mode

[Stephan Merz <stepha...@xxxxxxxxx>]

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

On Friday, February 10, 2017 at 3:05:54 AM UTC+1, Kirsten Winter wrote:

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

On 10/02/17 11:05, Leslie Lamport wrote:

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