Motivation:
I would like to define three variables in TLA+.The value of each variable is important only in that each is different from the others and is defined in the module, not in the model. I do not want to use something like a string, "Foo" or a Natural number, like 1, because then the values are visible. Part of my motivation is to better understand TLA+ and CHOOSE.
Detail:
Immediately CHOOSE comes to mind. However, I think an appropriate predicate would be required to ensure that the values are different from each other. I could create a predicate that compares the value chosen by CHOOSE, to a set containing my prior choices. (I think this is possible. Maybe make an empty set and add create an operator or function to make the CHOOSE, and add to the set...)
Is it true that in order to expect CHOOSE to always select a value unique from other values I obtained from CHOOSE, that I must provide a predicate to enforce this?
Is there a better way to accomplish what I want?
How is CHOOSE implemented?