Removing item taken from CHOOSE

[thomas...@gmail.com]

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?

[Alex Weisberger]

set' = set \ {CHOOSE e \in set: TRUE}

Is that what you're looking for?

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3c62cdf2-6ed4-4d1f-ae25-529bc6616cben%40googlegroups.com.

[thomas...@gmail.com]

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?

[Stephan Merz]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/21d17d43-ecfc-4812-96d7-b83f03056f35n%40googlegroups.com.

[thomas...@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!