Re: [tlaplus] BagOfAll? SetOfAll?

[Stephan Merz <Stepha...@xxxxxxxxx>]

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

On 05 Jun 2015, at 02:19, Chen Fu <chen...@xxxxxxxxx> wrote:

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

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