Re: [tlaplus] BagOfAll? SetOfAll?

[Chen Fu <chen...@xxxxxxxxx>]

This works great. Thanks!

On Friday, June 5, 2015 at 2:17:13 AM UTC-7, Stephan Merz wrote:

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 <che...@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...@googlegroups.com.
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.