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

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/be5ccdf7-ffa9-4b19-a37f-8cc0a7203ac6o%40googlegroups.com.