# Re: [tlaplus] Generating records like functions

• From: Jeremy Wright <jeremy@xxxxxxxxxxxx>
• Date: Mon, 3 Jan 2022 16:40:37 -0700
• Ironport-hdrordr: A9a23:YKDQSKtPbTh6d5hWl9T1im2T7skCAoAji2hC6mlwRA09TyXGrbHKoB1L726XtN9OYgBCpTnhAtjmfZquz+8F3WB3B8b2YOCGghr9EGgG1/qH/9SOIVyDygdi79Y2T0ETMqyLMbE+t7eF3OFXe+xQkeVu3siT9LTjJl1WPF5Xg5gJ1XYoNu5wencGFjWufKBJSqZ0hfA31AZIG05nE/hTXUN1A9Qrzuej/PmKDXFmZ29AmXCzZHGTmcXH+jejr0Ejulh0sOwfGAb+4nTED+mYwo6GIt617R6I03wA8+GRuudrNYinjM8JJjLwzimpYZlsQLGO+BskydvfsGrC3eO87isIDoBW0Tf8b2u1qRzi103J1ysv0WbrzRu9jWH4qcL0aTomA44Z7LgpPSfx2g4FhpVRwahL12WWu95+Cg7Bpj3045ztWwtxnkS5jHI+mao4jmBZU6EZdLhNxLZvsH99IdMlJmbX+YonGO5hAIX14+tXS0qTazTjsmxm0LWXLzwONybDZnJHlt2e0jBQknw85VAf3tYjknAJ8494Y4VY5szfW54Y141mf4szV+ZQFe0BScy4BijmWhTXKl+fJlzhCeUuJ2/NkZjq+784jdvaOKDg9KFC3agpbWko8VLbIynVeIqzNdxwg1HwqVyGLHbQIpo03ek+hlX+LICbeBFrBmpeyvdImM9vd/EzbczDTq6+M8WTX1cGJrw5qzEX1PFpWCQjue0uy50GsgG104j2wrODjJ2tTB+UHsuiLd/6YAmQPkc+

Hello jwnhy,

Do you mean something like this?

tlaplus

f == [x |-> {0, 1}, y |-> {4,5}]



On Mon, Jan 3, 2022 at 4:30 PM jwnhy <qq799433746@xxxxxxxxx> wrote:
Hello, I'm new to TLA+ and trying to learn it.

I know that I can generate a set of all possible functions by writing

[{"A", "B"} -> {0, 1}] \* all functions from {"A", "B"} to {0, 1}

I'm wondering if there is a similar way for records?

For example, if I have a record that most of its fields is BOOLEAN, I'm wondering if I can write something like

mstatus \in [{SD, TSR, TW, TVM}: BOOLEAN] \* THIS DOES NOT WORK

Or is there a way to specify a function with different range for different domain?

e.g: f["x"] \in {0,1} f["y"] \in {4, 5}

Thanks,
jwnhy.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.