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

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

On Thursday, November 23, 2023 at 1:49:44 PM UTC+1 ryanth...@xxxxxxxxx wrote:

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/bc26c608-9077-421f-a732-d9bb307cf748n%40googlegroups.com.
INIT Init
NEXT Next
CONSTANTS
    User = {alice, bob}
    Key = {a,b}
    Value = {"foo", "bar", "baz"}
INVARIANT TypeOK

Attachment: Test.tla
Description: Binary data