Re: [tlaplus] Variables with values unspecified but distinct from each other

If you intend your specification to be used with TLC, you have to use bounded choice (CHOOSE x \in S : ...), contrary to your goal of not specifying the kinds of these values.

My suggestion would be to declare constant parameters and assume they are distinct, like so:

CONSTANT x,y,z

ASSUME x # y /\ x # z /\ y # z

For a TLC model, you can instantiate these constants by model values, which are always distinct.

Stephan

On 26 Jul 2020, at 21:39, mmynsted <code@xxxxxxxxxxxxxxxxxx> wrote:

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?

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/25239a98-d60c-4d15-ad4f-6cce4964691fo%40googlegroups.com.

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9540F26C-5956-4912-8DD1-C62EA719B7AC%40gmail.com.