How to model a structure with sets as keys?

[Ryan Worsley]

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

[Stephan Merz]

Hi,

it looks like you are trying to represent a structure of the form

dict \in [User -> [(SUBSET Key) -> STRING]]

or – given that presumably the inner function is not total, i.e., you don't associate a string with every subset of keys – perhaps rather

dict \in [User -> (UNION {[D -> STRING] : D \in SUBSET (SUBSET Key)})]

and you are asking how to represent values of that structure in TLA+. For the representation of the outer function, you used record syntax

[ alice |-> ..., bob |-> ... ]

This works assuming that users are strings. If you use functions, you should have written something like

[ u \in User |-> IF u = alice THEN ... ELSE IF u = bob THEN ... ELSE ... ]

which gets a little tedious. Using the operators for finite functions defined in the TLC module you can instead write

(alice :> ...) @@ (bob :> ...) @@ ...

For the inner function, record syntax doesn't work because your arguments are definitely not strings but sets of keys.

A minimal working example of a specification based on these ideas is enclosed below.

Hope this helps,

Stephan

[Ryan Worsley]

Hi Stephan,

This is extremely helpful and given me lots of food for thought, I've also learned a bunch of new syntax that I wasn't aware of and am enjoying playing around with.

Many thanks,

Ryan