Re: [tlaplus] Re: Dictionary type

[Paul Eipper <lkra...@xxxxxxxxx>]

Hello,

I admit I was thinking of the second approach, but could not formalize it.

The partial function concept is what I was missing, thanks.


--
Paul Eipper


On Thu, Jun 19, 2014 at 6:34 PM, Dominik Hansen
<do.han...@xxxxxxxxxxxxxx> wrote:
> Hi,
>
> in TLA+ records are functions whereby the domain is a set of strings.
> Hence, the set of all records *with an arbitrary number of strings* is the
> set of partial functions mapping strings to strings.
> TLA+ has no built-in operator for partial functions and you have to define
> the operator by your own:
>
> ----------------------------- MODULE Test -----------------------------
> PartialFunctions(S, T) ==  UNION { [x -> T] : x \in SUBSET S}
> DictionaryType == PartialFunctions(STRING,STRING)
> \* TLC is not able to check if a certain function is in the DictionaryType
> \* ASSUME [key1 |-> "val1", key2 |-> "val2", key3 |-> "val3"] \in
> DictionaryType
> \* PartialFunctions should be used if S and T are finite (and small)
>
> inDictionaryType(f) ==
>     /\ DOMAIN(f) \subseteq STRING
>     /\ \A x \in DOMAIN f: f[x] \in STRING
> ASSUME inDictionaryType([key1 |-> "val1", key2 |-> "val2", key3 |-> "val3"])
>
> \* An alternative approach is to define the dictionary using sets of pairs
> instead of functions
> DictionaryType2 == { f \in SUBSET (STRING \times STRING): \A <<a,b>> \in
> f,<<c,d>> \in f: a=c => b = d }
> ASSUME {<<"key1","val1">>, <<"key2","val2">>, <<"key3", "val3">>} \in
> DictionaryType2
> ASSUME {<<"key1","val1">>, <<"key1","val2">>} \notin DictionaryType2
>
> GetValue(f,x) == (CHOOSE pair \in f: pair[1] = x)[2]
> ASSUME GetValue({<<"key1","val1">>, <<"key2","val2">>, <<"key3", "val3">>},
> "key2") = "val2"
> =============================================================================
>
> Regards,
> Dominik
>>
>>
> --
> 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+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.