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

*From*: "thomas...@xxxxxxxxx" <thomasgebert@xxxxxxxxx>*Date*: Mon, 1 Nov 2021 12:23:44 -0700 (PDT)*References*: <3c62cdf2-6ed4-4d1f-ae25-529bc6616cben@googlegroups.com> <CAEPrOmK_+GU5Wn78xJEftQRK8tKWxQODuEiw4q+B5sk+OfdJMg@mail.gmail.com> <21d17d43-ecfc-4812-96d7-b83f03056f35n@googlegroups.com> <8AD659AF-D1F0-448C-ACAB-5FD773CD71E9@gmail.com>

I think you're right, it would probably make sense to test every potential choice, one at a time. Thanks for the tips!

On Monday, November 1, 2021 at 2:21:23 PM UTC-4 Stephan Merz wrote:

If you need the element elsewhere in the definition of the action that removes it from the set, you can writeLET e == CHOOSE x \in set : TRUEIN /\ set' = set \ {e}/\ \* remainder of the actionIf you need e in a different action later in the execution, you will need to represent it as a state variable and you can write/\ e' = CHOOSE x \in set : TRUE/\ set' = set \ {e}/\ ...Note that CHOOSE picks an arbitrary but fixed element from the set: if the set contains {1,2,3} then TLC will generate one successor state in which the chosen element (say, 1) has been removed.If you wish to model check your system for all possible choices of elements, use an existential quantifier as in\E e \in set : set' = set \ {e}In the above example, TLC will explore three successor states corresponding to removing each of the elements.StephanOn 1 Nov 2021, at 19:11, thomas...@gmail.com <thomas...@xxxxxxxxx> wrote:I don't think that would work because I need access to e later in this system. Can I use e later if I do it that way?On Monday, November 1, 2021 at 2:05:50 PM UTC-4 alex.m.w...@gmail.com wrote:set' = set \ {CHOOSE e \in set: TRUE}Is that what you're looking for?Hi,I want to CHOOSE something out of a set. I don't particularly care what that item is, but I would like the ability to remove it from the set after I have gotten it.What's the best way of going about this?--

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...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3c62cdf2-6ed4-4d1f-ae25-529bc6616cben%40googlegroups.com.

--

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...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/21d17d43-ecfc-4812-96d7-b83f03056f35n%40googlegroups.com.

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/97f353c9-2f20-4d95-bc1b-d69c124b35a1n%40googlegroups.com.

**References**:**[tlaplus] Removing item taken from CHOOSE***From:*thomas...@xxxxxxxxx

**Re: [tlaplus] Removing item taken from CHOOSE***From:*Alex Weisberger

**Re: [tlaplus] Removing item taken from CHOOSE***From:*thomas...@xxxxxxxxx

**Re: [tlaplus] Removing item taken from CHOOSE***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Removing item taken from CHOOSE** - Next by Date:
**Re: [tlaplus] Trouble Verifying Sorting Property on A Simple Spec** - Previous by thread:
**Re: [tlaplus] Removing item taken from CHOOSE** - Next by thread:
**[tlaplus] How to specify broadcasting a message** - Index(es):