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

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.

Best regards,
Jaak


• Follow-Ups:
• References: