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

[yati sagade <yati.sagade@xxxxxxxxx>]

Thanks Stephen and Hillel for the pointers!

-yati

On Thu, Feb 7, 2019 at 7:02 AM Hillel Wayne <HWayne@xxxxxxxxx> wrote:
>
> 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.

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