[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Assign tuple to a constant


I have written some TLA+ specifications that use constant tuples. I am able to assign a tuple e.g. ` << {1}, {2}, {3} >> ` to a constant in the toolbox (works as expected). But when I try to do the same in a config file for the command line tools e.g. ` CONSTANT Someconstant =  << {1}, {2}, {3} >> ` I get the following error:

TLC found an error in the configuration file at line (tuple assignment line)
It was expecting = or <-, but did not find it.

So I would like to know if and how a tuple can be assigned to a constant in the config file.

The motivation for using the command line tools is that I would like to automatically generate different config files and use them to check the model. Any suggestions for doing this with the toolbox will also be helpful.