CODEWITHSUNDEEP
tla+
red27bull
red27bull

Reputation: 33

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+?

Upvotes: 2

Views: 1033

Answers (1)

Hovercouch
Hovercouch

Reputation: 2314

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".)

Upvotes: 2

Related Questions