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

*From*: mmynsted <code@xxxxxxxxxxxxxxxxxx>*Date*: Mon, 27 Jul 2020 14:43:18 -0700 (PDT)*References*: <25239a98-d60c-4d15-ad4f-6cce4964691fo@googlegroups.com> <c14403e0-1e14-4a45-8d3a-b8815c478781o@googlegroups.com> <0c5fc561-5dc9-46ea-acd5-88177a5ceb33n@googlegroups.com> <be5ccdf7-ffa9-4b19-a37f-8cc0a7203ac6o@googlegroups.com>

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 .. nS(n) == F[n]P(Q) == CHOOSE n \in S(Cardinality(Q) + 1) : n \notin QRed == 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 formx == CHOOSE b : b \notin Sthen 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 writex == 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/9f89ec66-a16c-4d89-b0df-3c685b856665n%40googlegroups.com.

**References**:**[tlaplus] Variables with values unspecified but distinct from each other***From:*mmynsted

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

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

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

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