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的下一个状态值”)。