tla+ - 一组对，有和没有重复

Question

我有两套:

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

我想生成以下一组对:

{<<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>>}

在每个集合中，第一个元素来自 X，第二个元素来自 Y。X 可以重复，Y 不能。怎么做？

Answer 1

使用 \X运算符为我们提供了所有对的集合:X \X Y = {<<a, 1>>, <<a, 2>>, ... <<b, 3>>} . SUBSET (X \X Y)给了我们所有可能的集合。 {s \in SUBSET (X \X Y): Cardinality(s) = 3} (来自 FiniteSets 模块)为我们提供了所有 3 元素集。

我们希望在每对的第二个元素上使它唯一。让我们定义一个新的运算符:

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

如果我们这样做 {x[2] : x \in {<<a, 1>>, <<a, 2>>, <<a, 2>>}} ，我们得到 {1, 2} ，它的基数较小，将被过滤掉。所以我们最后的表达是

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

注意没有基数检查{<<a, 1>>}将是集合集合的一部分，这不是您要查找的内容。