# Re: [tlaplus] How to choose a record field when a record is an element of a set?

> On 12 Nov 2015, at 09:25, Jaak Ristioja <jaak.r...@xxxxxxxx> wrote:
>
> On 11.11.2015 18:50, Y2i wrote:
>> Looking for a practical advice...
>>
>> Let's assume I'm reading a record by its ID.  There is at most one record
>> with such an ID.
>>
>> TypeInvariant == \A d \in data : Cardinality({x \in data : x.id = d.id}) = 1
>>
>>
>> If such record exists, I need to return its *d* field.  I currently use
>> CHOOSE to select such a record:
>>
>>
>> R(r) == CHOOSE x \in r : TRUE
>>
>>
>>
>>    /\ r.op = "R"
>>
>>    /\ LET d == {x \in data : x.id = r.id}
>>
>>       IN  IF d = {} THEN
>>
>>               qout' = Append(qout, [code|->"ERR"])
>>
>>           ELSE
>>
>>               qout' = Append(qout, [code|->"OK", d|->R(r).d])
>>
>>    /\ UNCHANGED <<data>>
>>
>>
>> Is there a  better way to achieve this?
>
> I recently had similar questions and found no better way to do it than
> what you just demonstrated. In the end, I found that converting the sets
> to records with the ID as the domain was a better overall solution for
> me. To check whether an element with the ID in is in the record, one
> just has to check (id \in DOMAIN theSet), and use theSet[id] to retrieve
> it. This looks a lot nicer when written in TLA+, but I'm not sure how it
> affects TLC/TLAPS performance.

That's indeed the canonical TLA+ idiom: represent functional dependency by functions.

Stephan



• Follow-Ups:
• References: