3

我有两套：

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 不能。怎么做？

4

2 回答 2

2

使用\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>>}，它将成为集合集的一部分，这不是您要寻找的。

于 2017-12-14T23:33:24.930 回答
1 
EXTENDS Functions, FiniteSets, Naturals

CONSTANTS a, b

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

Dom == 1..Cardinality(Y)

Slice == {{<< xt[n], yt[n] >>:  n \in Dom}:
              << xt, yt >> \in [Dom -> X] \X Bijection(Dom, Y)}

TLAPS 发行版包括模块Functions。模块FiniteSets和Naturals是 TLA+ 标准库的一部分。

于 2017-12-15T13:46:32.570 回答