How can I assign sequences to constants in the CONSTANTS section of a TLA+ configuration file?
-
04-10-2019 - |
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?
Solution
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.
OTHER TIPS
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.