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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 24 Dec 2019 09:55:15 +0100*References*: <076e423b-fe5b-4046-a9c4-bb7077e80f01@googlegroups.com> <3C7DBF0C-D094-4360-97B0-C1BA42D07103@gmail.com> <67e9079a-443d-4b28-a9f2-36ac7378d36f@googlegroups.com>

Below are definitions TLA+ operators that convert a set of integers into a sorted sequence. You can take the first N elements of SortedSeqFromSet(Range(f)) to retrieve the N smallest values of the function f. Evaluation of these operators still requires quadratic time, and although you could write a Quicksort operator in TLA+, if you really care about efficiency you should probably consider overriding the definition of SortedSeqFromSet(_) by a Java method. Best, Stephan RECURSIVE InsertSorted(_,_,_), SortedSeqFromSet(_) InsertSorted(x, seq, i) == \* insert element in a sorted sequence of integers, starting from index i IF i > Len(seq) THEN seq \o << x >> ELSE IF x <= seq[i] THEN SubSeq(seq, 1, i-1) \o << x >> \o SubSeq(seq, i, Len(seq)) ELSE InsertSorted(x, seq, i+1) SortedSeqFromSet(S) == \* convert a set of integers into a sorted sequence IF S = {} THEN << >> ELSE LET x == CHOOSE x \in S : TRUE rest == SortedSeqFromSet(S \ {x}) IN InsertSorted(x, rest, 1)
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/826397D5-5C3D-42AF-A560-B019523B5411%40gmail.com. |

**References**:**[tlaplus] TLA+ minimum of function/sequence***From:*Thomas Gebert

**Re: [tlaplus] TLA+ minimum of function/sequence***From:*Stephan Merz

**Re: [tlaplus] TLA+ minimum of function/sequence***From:*Thomas Gebert

- Prev by Date:
**Re: [tlaplus] TLA+ minimum of function/sequence** - Next by Date:
**[tlaplus] Optimizing for model checking** - Previous by thread:
**Re: [tlaplus] TLA+ minimum of function/sequence** - Next by thread:
**[tlaplus] Optimizing for model checking** - Index(es):