Operations on a sequence of records

31 views
Skip to first unread message

Felipe Lisboa

unread,
Feb 23, 2021, 6:59:27 AM2/23/21
to tlaplus
Hi,

My problem is the following:

A have a sequence of many instances of a record. Like this
seq_of_records == <<rec1,rec2,rec3>> 

Where every record has the same type (same fields), but different values for each.

I have to find the minimum value of a certain field between all the instances of that record. Something like:
min_value = min(rec1.a,rec2.a,rec3.a)

I tried:
new_sequence == SelectSeq(seq_of_records, LAMBDA element: element.a)
transform_to_set == ToSet(new_sequence)
min_value = Min(transform_to_set)

But that use of the LAMBDA operator does not seems to be valid. Any tip on how to get just some fields from a sequence of records ?

Thanks

Stephan Merz

unread,
Feb 23, 2021, 7:56:46 AM2/23/21
to tla...@googlegroups.com
The second argument of SelectSeq is expected to be a predicate (a Boolean-valued operator). In order to retrieve the set of record fields, simply write

{ seq_of_records[i].a : i \in 1 .. Len(seq_of_records) }

Stephan

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e402108b-3d4a-4ade-b94c-ad42e152295an%40googlegroups.com.

Felipe Lisboa

unread,
Feb 26, 2021, 8:42:27 AM2/26/21
to tlaplus
Hi Stephan

Thanks for the answer !

Felipe
Reply all
Reply to author
Forward
0 new messages