如何将序列分配给TLA+配置文件的常数部分中的常数？

Question

我试过了

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

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

错误：TLC在第1行的配置文件中发现了一个错误。它预期=或< - 没有找到它。

我还试图包括 Sequences 配置文件中的模块，无济于事。

那么...我该怎么做才能分配序列？

Answer 1

我不记得曾经面临过这个问题，我的TLC太生锈了，无法尝试给您第一手答案（我只是使用TLA+工具箱重新启动）。

但是，从帖子链接的波纹管中，我认为您无法通过TLC配置文件实例化序列。

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

即使问题是旧的，答案也可能有助于未来的Tlaers。

Answer 2

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