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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Mon, 27 Jul 2020 08:32:46 +0200*References*: <25239a98-d60c-4d15-ad4f-6cce4964691fo@googlegroups.com>

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 <code@xxxxxxxxxxxxxxxxxx> 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9540F26C-5956-4912-8DD1-C62EA719B7AC%40gmail.com. |

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] Variables with values unspecified but distinct from each other** - Next by Date:
**Re: [tlaplus] Variables with values unspecified but distinct from each other** - Previous by thread:
**[tlaplus] Variables with values unspecified but distinct from each other** - Next by thread:
**Re: [tlaplus] Variables with values unspecified but distinct from each other** - Index(es):