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

*From*: Paul Eipper <lkra...@xxxxxxxxx>*Date*: Mon, 23 Jun 2014 14:47:02 -0300*References*: <CAO8R-xh4c_EqFXKLVo10JD5e6WTQdvqKX+SqeDy16t3LTF5kDg@mail.gmail.com> <b9e217c4-8612-45d5-a165-1b21da3d0da5@googlegroups.com>

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.

**References**:**Dictionary type***From:*Paul Eipper

**Re: Dictionary type***From:*Dominik Hansen

- Prev by Date:
**Parsing Error in Consensus.tla** - Next by Date:
**"Partial" Functions** - Previous by thread:
**Re: Dictionary type** - Next by thread:
**Parsing Error in Consensus.tla** - Index(es):