Variables with values unspecified but distinct from each other

[mmynsted]

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?

[Stephan Merz]

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...@growingliberty.com> wrote:



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

[mmynsted]

What I like about:

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. 

Building toward what I want . . . 

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} 

This appears to work but is not ideal. 

- I am explicitly adding to the binding predicate, for what n can not be. There should be a way to have a function or something do this automatically right? 

- I am explicitly providing a finite, enumerable set, of numbers. I do not know how to define a finite set of values of some undetermined type.

I also notice that because my approach is not constant, Red is evaluated every time it is used. (I am fine with the evaluation each use, since I think that is simply how TLA+ works.)

[Leslie Lamport]

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

[mmynsted]

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.

[Leslie Lamport]

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

[mmynsted]

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.