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

Yes! Thank you.  :-)

I see that when I created a new model the MC.cfg file generated differently. That file included:
CONSTANT
Red = Red
Yellow = Yellow
Green = Green

I was able to replicate the incantation for the older model by altering the "Definition Override" from the "Spec Options" to use the model value for each.

Now I will try to make this into an operator.

Thanks again.

On Monday, July 27, 2020 at 3:52:20 PM UTC-5 Leslie Lamport wrote:
If you put the definitions in my post in your spec and TLC reported the error you mentioned, then
you failed to pay attention to the words "when you create a model for it" in my post.

Leslie

On Monday, July 27, 2020 at 12:48:07 PM UTC-7, mmynsted wrote:
Thank you.
For some reason if I do not bind the CHOOSE like:

x == CHOOSE a \in S : a \notin {}

Then I get an error "TLC attempted to evaluate an unbounded CHOOSE"
So something like this is closer to what I am after.

F[n \in Nat] == 0 .. n
S(n) == F[n]
P(Q) == CHOOSE n \in S(Cardinality(Q) + 1) : n \notin Q

Red == P({})
Yellow == P({Red})
Green == P({Red, Yellow})
Foo == P({Red, Yellow, Green})

I will try to simplify that F, S, and P bits... It seems like I should be able to use LET, In to combine those into a single operator.

On Monday, July 27, 2020 at 1:00:34 PM UTC-5 Leslie Lamport wrote:
If your spec contains a definition of the form

x == CHOOSE b : b \notin S

then when you create a model for it, the Toolbox will add to the model the appropriate
incantation to substitute for x a model value named "x".  You could therefore write

x == CHOOSE a : a \notin {}
y == CHOOSE a : a \notin {x}
z == CHOOSE a : a \notin {x,y}

and you won't have to do any instantiation of constants.

Leslie

--
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.