[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: mmynsted <code@xxxxxxxxxxxxxxxxxx>*Date*: Sun, 26 Jul 2020 12:39:37 -0700 (PDT)

Motivation:

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.

**Follow-Ups**:**[tlaplus] Re: Variables with values unspecified but distinct from each other***From:*Leslie Lamport

**Re: [tlaplus] Variables with values unspecified but distinct from each other***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?** - Next by Date:
**Re: [tlaplus] Variables with values unspecified but distinct from each other** - Previous by thread:
**[tlaplus] Re: The rules of TLA+ do not imply that 1 /= "a" ?** - Next by thread:
**Re: [tlaplus] Variables with values unspecified but distinct from each other** - Index(es):