Search code examples
tla+

Set of pairs, with and without repetitions

I have two sets:

X = {a, b}
Y = {1, 2, 3}

I would like to generate the following set of sets of pairs:

{<<a, 1>>, <<a, 2>>, <<a, 3>>}
{<<a, 1>>, <<a, 2>>, <<b, 3>>}
{<<a, 1>>, <<b, 2>>, <<a, 3>>}
{<<a, 1>>, <<b, 2>>, <<b, 3>>}
...
{<<b, 1>>, <<b, 2>>, <<b, 3>>}

In each set the first element is from X and the second is from Y. X can be repeated, Y cannot. How to do it?

Solution

  • Using the \X operator gives us the set of all pairs: X \X Y = {<<a, 1>>, <<a, 2>>, ... <<b, 3>>}. SUBSET (X \X Y) gives us all possible sets. {s \in SUBSET (X \X Y): Cardinality(s) = 3} (from the FiniteSets module) gives us all 3-element sets.

    We want to make this unique on the second element of each pair. Let's define a new operator: 

    UniqueBy(set, Op(_)) == Cardinality(set) = Cardinality({Op(s): s \in set})

    If we do {x[2] : x \in {<<a, 1>>, <<a, 2>>, <<a, 2>>}}, we get {1, 2}, which has a smaller cardinality and will be filtered out. So our final expression is

    {s \in SUBSET (X \X Y) : UniqueBy(s, LAMBDA x: x[2]) /\ Cardinality(s) = 3}

    Note that without the cardinality check {<<a, 1>>} would be part of the set of sets, which isn't what you're looking for.