tla+ - 比较 TLA+ 中的序列元素和集合

Question

给定一个序列 S = <<1,2,3,4>> 和一个集合 S' = {1,2,3,4,5,6}。我们如何检查它们是否在 TLA+ 中包含相同的值？

Answer 1

定义Range(f) == {f[x]: x \in DOMAIN f}. 由于所有序列都是函数，Range(S)因此会给我们序列 S 的值。然后我们检查两者是否具有相同的元素Range(S) = S_prime。

（我们不能这样称呼它，S'因为这意味着“下一个状态值S”。）