[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Generating a set of structs where each key ranges over a distinct set



The Bags module has SubBag(B), which is almost what you want, except it starts at 1, not 0. But the algorithm it uses can be easily adapted for your purpose. EXTENDS Bags and hit F3 to go to its definition.

On Tuesday, 5 February 2019 01:19:06 UTC-6, yati sagade wrote:
Given a structure like this:

    Inventory == [foo |-> 3, bar |-> 2, baz |-> 5] \* How much of an item do we have in store

I'd like to generate the set of structures

    AllPossibleShipments ==
        [foo: 0..3, bar: 0..2, baz: 0..5]

But of course without re-enumerating the items by hand. The most natural thing that came to mind is:

    AllPossibleShipments ==
        [item \in DOMAIN Inventory : 0..Inventory[item]]

That does not work. Any ideas?

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