0

我试过了

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

但 TLC 给了我一个语法错误：

错误：TLC 在第 1 行的配置文件中发现错误。它需要 = 或 <-，但没有找到。

我也尝试将Sequences模块包含在配置文件中，但无济于事。

那么......我必须做些什么来分配一个序列？

4

3 回答 3

2

我不记得曾经遇到过这个问题，而且我的 TLC 太生疏了，无法尝试给你第一手的答案（我刚刚使用 TLA+ 工具箱重新启动）。

但是，从下面链接的帖子中，我认为您无法通过 TLC 配置文件使用序列实例化常量。

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

尽管这个问题很老，但留下答案可能会对未来的 TLAers 有所帮助。

于 2011-02-17T12:03:28.530 回答
1

所以事实证明你需要一个单独的.tla文件。假设您有“Main.tla”作为源文件。你想MyConst拥有价值<<1,2,3>>。TLA+ 工具箱生成MC.tla放置常量的位置：

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

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

中MC.cfg，会有这条线

CONSTANT MyConst <- const_uniq12345

请注意，这MyConst = const_uniq12345不起作用 - 如果您使用=而不是<-，MyConst将包含模型值const_uniq12345而不是<<1, 2, 3>>

我使用https://github.com/hwayne/tlacli能够从命令行运行 TLC（TLA 工具箱有糟糕的 UX），并且我能够在.tla像这样的额外文件的帮助下提供一个元组常量。当然，我使用了有意义的名称而不是const_uniq12345太。java -cp /path/to/tla2tools.jar ...但是，必须手动调用（使用--show-script选项获得完整命令tlacli），因为当前tlacli无法<-在配置中处理。

于 2020-05-02T18:36:23.443 回答
1

您不能直接分配给 TLA+ 文件中的常量。如果您使用工具箱，请编写CONSTANTS seq，然后在模型中添加您想要的元组作为普通作业。

于 2018-02-01T22:59:01.330 回答