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

[tlaplus] How to generate a sequence from another sequence ?


I have a sequence of records with field `id`. I want to get a sequence of all ids from original sequence.

My first attempt was to try this :
[r \in some_sequence_of_records |-> r.id]

"The exception was a java.lang.RuntimeException
: util.Assert$TLCRuntimeException: The domains of formal parameters must be enumerable.
The error occurred when TLC was evaluating the nested
expressions at the following positions:
    The error call stack is empty."

Q1. Is "some_sequence_of_records" a set with DOMAIN 1..Len(sequence) ?
Q2. What is wrong with my first try ?

Currently, i am using custom map and filter functions for the sequences.

RECURSIVE mapSeq(_,_,_)
mapSeq(seqs, M(_), result) ==
    IF seqs = <<>>
    THEN result
    ELSE mapSeq(Tail(seqs),
                   Append(result, M(Head(seqs))))

GetAllIds(files) ==
    LET getId(r) == r.id
    IN mapSeq(files, getId, <<>>)

Q3. Is there a better way ?


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/5f09aa29-391f-49f1-833f-c6200fa2450co%40googlegroups.com.