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

[Stephan Merz <stepha...@xxxxxxxxx>]

> 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
>> 
>> 
>> 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.

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

Stephan