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

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

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
> 
> 
> Read(r) ==
> 
>     /\ 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