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.