如何将序列分配给 TLA 的 CONSTANTS 部分中的常量？配置文件？
我已经尝试过
CONSTANTS seq = <<5,6,7>>
，但 TLC 给了我一个语法错误：
错误：TLC 发现错误 配置文件的第 1 行。它是 期待 = 或 <- 但没有找到。
我还尝试在配置文件中包含 Sequences 模块，但无济于事。
那么...我需要做什么来分配序列？
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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
我不记得曾经遇到过这个问题，而且我的 TLC 太生锈了，无法尝试为您提供第一手答案（我刚刚重新使用 TLA+ 工具箱）。
然而，从下面链接的帖子中，我发现您无法通过 TLC 配置文件使用序列实例化常量。
http://bbpress.tlaplus.net/topic/creating-a -sequence-from-a-set
尽管问题很老，留下答案可能会对未来的 TLAers 有所帮助。
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.
您不能直接分配给 TLA+ 文件中的常量。如果您使用工具箱，请编写
CONSTANTS seq，然后在模型中添加所需的元组作为普通赋值。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.所以事实证明您需要一个单独的
.tla文件。假设您有“Main.tla”作为源文件。您希望MyConst具有值<<1,2,3>>。 TLA+ 工具箱生成MC.tla，其中放置常量：在
MC.cfg中，将会有一行Note that
MyConst = const_uniq12345won'不起作用 - 如果您使用=而不是<-，MyConst将包含模型值const_uniq12345而不是<<1, 2, 3>>我使用了 https://github .com/hwayne/tlacli 能够从命令行运行 TLC（TLA 工具箱的用户体验很糟糕），并且我能够在额外的 .tla 文件的帮助下提供元组常量像这样。当然，我也使用了有意义的名称而不是
const_uniq12345。不过，必须手动调用java -cp /path/to/tla2tools.jar ...（使用的），因为当前--show-script选项获取完整命令tlaclitlacli不处理配置中的<-。So it turns out that you need a separate
.tlafile for that. Suppose you have "Main.tla" as you source file. You wantMyConstto have value<<1,2,3>>. TLA+ toolbox generatesMC.tlawhere it puts the constants:in
MC.cfg, there will be the lineNote that
MyConst = const_uniq12345won't work -- if you use=instead of<-,MyConstwill contain model valueconst_uniq12345instead 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
.tlafile like this. I used meaningful name instead ofconst_uniq12345too, of course. Had to calljava -cp /path/to/tla2tools.jar ...manually, though (got the full command using--show-scriptoption oftlacli), because currentlytlaclidoesn't handle<-in the config.