如何用TLA+生成指定键值集合的全部可能记录？

背景 #

已定义如下TLA+基础集合：

keyset == {"k1", "k2"}
valueset == {"v1", "v2"}

需要生成包含全部4种可能记录的集合。

实现方案 #

方法一：利用函数集合语法（推荐） #

TLA+中的记录本质是定义域为字符串集合的函数，因此可以直接使用函数集合构造器[S -> T]生成所有符合要求的记录。该构造器会生成所有从集合S映射到集合T的函数，对应所有可能的记录组合。

完整代码：

keyset == {"k1", "k2"}
valueset == {"v1", "v2"}
AllPossibleRecords == [keyset -> valueset]

方法二：集合推导式 #

如果需要更直观的构造逻辑，可以用集合推导式枚举所有值的组合，手动构造记录：

keyset == {"k1", "k2"}
valueset == {"v1", "v2"}
AllPossibleRecords == { [k1 |-> a, k2 |-> b] : a ∈ valueset, b ∈ valueset }

结果验证 #

两种方法生成的结果完全一致，均为目标集合：

{
  [k1 |-> v1, k2 |-> v1],
  [k1 |-> v1, k2 |-> v2],
  [k1 |-> v2, k2 |-> v1],
  [k1 |-> v2, k2 |-> v2]
}

内容的提问来源于stack exchange，提问作者Tauta