Re: [tlaplus] Removing item taken from CHOOSE

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 write

LET e == CHOOSE x \in set : TRUE
IN /\ set' = set \ {e}
/\ \* remainder of the action

If 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.

Stephan

On 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?

On Mon, Nov 1, 2021 at 1:56 PM thomas...@xxxxxxxxx <thomas...@xxxxxxxxx> wrote:

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.