[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Felipe Lisboa <lisboafelipe5@xxxxxxxxx>*Date*: Fri, 26 Feb 2021 05:42:26 -0800 (PST)*References*: <e402108b-3d4a-4ade-b94c-ad42e152295an@googlegroups.com> <EFAAABA7-34E0-49A5-A8CC-8AE8F1A1BD75@gmail.com>

Hi Stephan

Thanks for the answer !

Felipe

Em terça-feira, 23 de fevereiro de 2021 às 13:56:46 UTC+1, Stephan Merz escreveu:

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) }StephanOn 23 Feb 2021, at 12:35, Felipe Lisboa <lisboa...@xxxxxxxxx> wrote:Hi,

My problem is the following:

A have a sequence of many instances of a record. Like thisseq_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--

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e402108b-3d4a-4ade-b94c-ad42e152295an%40googlegroups.com.

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d648a9a3-a031-4524-a654-5dbc8d4fd104n%40googlegroups.com.

**References**:**[tlaplus] Operations on a sequence of records***From:*Felipe Lisboa

**Re: [tlaplus] Operations on a sequence of records***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC** - Next by Date:
**[tlaplus] Checking Real Time Systems and TLA+** - Previous by thread:
**Re: [tlaplus] Operations on a sequence of records** - Next by thread:
**[tlaplus] Checking Real Time Systems and TLA+** - Index(es):