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

*From*: Hillel Wayne <HWayne@xxxxxxxxx>*Date*: Wed, 6 Feb 2019 22:02:44 -0800 (PST)*References*: <b31f11b3-0c7d-45b4-a23e-5e0ce8f3440d@googlegroups.com>

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:

-- 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.

**Follow-Ups**:

**References**:**Generating a set of structs where each key ranges over a distinct set***From:*yati sagade

- Prev by Date:
**[tlaplus] Re: Practical TLA+ now out** - Next by Date:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Previous by thread:
**Re: [tlaplus] Generating a set of structs where each key ranges over a distinct set** - Next by thread:
**Re: [tlaplus] Re: Generating a set of structs where each key ranges over a distinct set** - Index(es):