How can I assign sequences to constants in the CONSTANTS section of a TLA+ configuration file?
I've tried
CONSTANTS seq = <<5,6,7>>
but TLC gives me a syntax error:
开发者_JAVA百科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?
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.
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.
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.
精彩评论