[tlaplus] How to model a structure with sets as keys?

[Ryan Worsley <ryanthemadone@xxxxxxxxx>]

Hi,

I'm new here and just learning TLA+, but loving the journey so far. I've made lots of progress without help, but have hit a snag that I'd really appreciate some advice on.

It's regarding the best way to model some data, I've got a situation where for a bunch of users I need to capture their information about some constants;

a, b, c, ...

Such that for any combination of these constants I have a structure similar to

[

    alice |-> [{a, b} |-> "foo", {a} |-> "bar"],

    bob   |-> [{b} |-> "baz", {b, c} |-> "boz"]

]

My initial attempt was as the above and just tried to use sets as keys into the structure, but it appears this isn't valid syntax.  I've also toyed with something like the following

[

    alice |-> {<<{a, b}, "foo">>, <<{a}, "bar">>},

    bob   |-> {<<{b}, "baz">>, <<{b, c}, "boz">>}

]

This probably works, but I've thrown my hands up in despair because this doesn't feel like a clean data modelling.

I've also thought about defining this as a function and then overriding different keys as necessary, but I don't quite know how to do that and before investing any more time I thought I should ask for help.

Ultimately I'd like to be able to reduce the structure to give me the set of all strings keyed by any subset of the constants.

Can someone help me figure out the right way to go with this? Is there some key understanding that I'm missing?

Kind regards,

Ryan

-- 
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0349f711-3193-4da4-abc8-085a1b4741fan%40googlegroups.com.