tla+

Generate a set of all possible records in TLA+

Suppose

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

I want to generate a set of all 4 possible record

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

  • Use a function set:

    AllKVs == [keyset -> valueset]