[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Dictionary type


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"