| 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
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/8AD659AF-D1F0-448C-ACAB-5FD773CD71E9%40gmail.com. |