How can I assign sequences to constants in the CONSTANTS section of a TLA+ configuration file?

Question

I've tried

CONSTANTS seq = <<5,6,7>>

but TLC gives me a syntax error:

Error: TLC found an error in the configuration file at line 1. It was expecting = or <- and didn't find it.

I've also tried to include the Sequences module in the configuration file, to no avail.

So... what do I have to do to assign a sequence?

Answer 1

I don't remember ever facing this problem and my TLC is too rusty to try and give you a first hand answer (I just restarted using the TLA+ toolbox).

From the post linked bellow, however, I figure that you can't instantiate constants with sequences through the TLC config files.

http://bbpress.tlaplus.net/topic/creating-a-sequence-from-a-set

Even though the question is old, leaving an answer may help future TLAers.

Answer 2

You can't directly assign to a constant in the TLA+ file. If you're using the toolbox, write CONSTANTS seq, then in the model add the tuple you want as an ordinary assignment.

Answer 3

So it turns out that you need a separate .tla file for that. Suppose you have "Main.tla" as you source file. You want MyConst to have value <<1,2,3>>. TLA+ toolbox generates MC.tla where it puts the constants:

---- MODULE MC ----
EXTENDS Main, TLC

const_uniq12345 = <<1,2,3>>
====

in MC.cfg, there will be the line

CONSTANT MyConst <- const_uniq12345

Note that MyConst = const_uniq12345 won't work -- if you use = instead of <-, MyConst will contain model value const_uniq12345 instead of <<1, 2, 3>>

I used https://github.com/hwayne/tlacli to be able to run TLC from command line (TLA toolbox has awful UX), and I was able to supply a tuple constant with help of extra .tla file like this. I used meaningful name instead of const_uniq12345 too, of course. Had to call java -cp /path/to/tla2tools.jar ... manually, though (got the full command using --show-script option of tlacli), because currently tlacli doesn't handle <- in the config.