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

CONSTANT x,y,z

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

Thank you. I like that it is clear that the values are immutable and that they are different from each other. What I do not like is that I must set a value to each of them in the model. One of my motivations is to prevent the need for me to define the values in the model. Also the ASSUME could get rather long if I should need to define very many of these.

EXTENDS TLC, Naturals, Sequences, FiniteSets

S == 0 .. 9 \* something enumerable and simple

Red == CHOOSE n \in S : TRUE \* arbitrary value in S

Yellow == CHOOSE n \in S: Print(Red, TRUE) /\ n \notin {Red} \* arbitrary value in S that is not used. Show Red

Green == CHOOSE n \in S: n \notin {Red, Yellow} \* Pick anything in S that is not already used

Foo == CHOOSE n \in S: n \notin {Red, Yellow, Green}

On Monday, July 27, 2020 at 1:32:52 AM UTC-5 Stephan Merz wrote:

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