Search code examples
tla+

Comparing elements of sequence and set in TLA+

Given a sequence S = <<1,2,3,4>> and a set S' = {1,2,3,4,5,6}. How do we check if both of them contain the same values in TLA+?

Solution

  • Define Range(f) == {f[x]: x \in DOMAIN f}. Since all sequences are functions, Range(S) will give us the values of sequence S. Then we check both have the same elements with Range(S) = S_prime.

    (We can't call it S' because that means "The next state value of S".)