BagOfAll? SetOfAll?

[Chen Fu]

Hi:

I found a usage of BagOfAll in section 4 of "Real Time is Really Simple", where it appears to enable an action to be applied on every item in a bag.

I tried to dig in the documents, and also search online but can not find any other mentioning of the construct BagOfAll.

Is it still supported? What about a SetOfAll for a set?

Thanks!

Chen

[Stephan Merz]

The BagOfAll operator is defined in the Bags standard module (cf. section 18.3 of Specifying Systems). You can define the set analogue as

SetOfAll(F(_), S) == { F(x) : x \in S }

but it is probably just as easy to write the right-hand side directly.

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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Chen Fu]

This works great. Thanks!