From 646bd42ddb86256a1c507872d1f4ec6a91fedeff Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Thu, 15 Aug 2024 15:54:01 +0200 Subject: [PATCH 1/7] Sort the best traces as we go using insertion sort instead of sorting the whole array each time --- quint/src/runtime/trace.ts | 94 ++++++++++++++++++++++++++------------ 1 file changed, 65 insertions(+), 29 deletions(-) diff --git a/quint/src/runtime/trace.ts b/quint/src/runtime/trace.ts index e2efa9311..aca2f12ef 100644 --- a/quint/src/runtime/trace.ts +++ b/quint/src/runtime/trace.ts @@ -329,46 +329,48 @@ class TraceRecorderImpl implements TraceRecorder { const traceWithSeed = { frame: traceToSave, seed: this.runSeed } - this.bestTraces.push(traceWithSeed) - this.sortTracesByQuality() + this.insertTraceSortedByQuality(traceWithSeed) + // Remove the worst trace (if there more traces than needed) if (this.bestTraces.length > this.tracesToStore) { this.bestTraces.pop() } } - private sortTracesByQuality() { - const fromResult = (r: Maybe) => { - if (r.isNone()) { - return true - } else { - const rex = r.value.toQuintEx({ nextId: () => 0n }) - return rex.kind === 'bool' && !rex.value - } + private insertTraceSortedByQuality(trace: Trace) { + if (this.bestTraces.length === 0) { + // This is the first trace, just add it + this.bestTraces.push(trace) + return } - this.bestTraces.sort((a, b) => { - // Prefer short traces for error, and longer traces for non error. - // Therefore, trace a is better than trace b iff - // - when a has an error: a is shorter or b has no error; - // - when a has no error: a is longer and b has no error. - const aNotOk = fromResult(a.frame.result) - const bNotOk = fromResult(b.frame.result) - if (aNotOk) { - if (bNotOk) { - return a.frame.args.length - b.frame.args.length - } else { - return -1 - } - } else { - // a is ok - if (bNotOk) { - return 1 + // Compute the index where the trace should be inserted, + // using a binary search over the already sorted traces. + const insertionIndex = (() => { + var low = 0 + var high = this.bestTraces.length - 1 + + while (low < high) { + // The index of the middle element in the range that remains to be searched + const mid = (low + high) >>> 1 // Math.floor((low + high) / 2) + + // Compare the trace to insert with the trace at the middle index + if (compareTracesByQuality(trace, this.bestTraces[mid]) < 0) { + // The trace to insert is better than the trace at the middle index, + // so we continue searching in the left half of the range + high = mid } else { - return b.frame.args.length - a.frame.args.length + // The trace to insert is worse than the trace at the middle index, + // so we continue searching in the right half of the range + low = mid + 1 } } - }) + + return low + })() + + // Insert the trace at the computed index + this.bestTraces.splice(insertionIndex, 0, trace) } // create a bottom frame, which encodes the whole trace @@ -385,3 +387,37 @@ class TraceRecorderImpl implements TraceRecorder { } } } + +// Compare two traces by quality. +// +// Prefer short traces for error, and longer traces for non error. +// Therefore, trace a is better than trace b iff +// - when a has an error: a is shorter or b has no error; +// - when a has no error: a is longer and b has no error. +function compareTracesByQuality(a: Trace, b: Trace): number { + const fromResult = (r: Maybe) => { + if (r.isNone()) { + return true + } else { + const rex = r.value.toQuintEx({ nextId: () => 0n }) + return rex.kind === 'bool' && !rex.value + } + } + + const aNotOk = fromResult(a.frame.result) + const bNotOk = fromResult(b.frame.result) + if (aNotOk) { + if (bNotOk) { + return a.frame.args.length - b.frame.args.length + } else { + return -1 + } + } else { + // a is ok + if (bNotOk) { + return 1 + } else { + return b.frame.args.length - a.frame.args.length + } + } +} From 927dd9419ca64ba979f86b861e854dc148afc7ee Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Thu, 15 Aug 2024 16:36:42 +0200 Subject: [PATCH 2/7] Fix bug in sorted insertion function --- quint/src/runtime/trace.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/quint/src/runtime/trace.ts b/quint/src/runtime/trace.ts index aca2f12ef..9939c408f 100644 --- a/quint/src/runtime/trace.ts +++ b/quint/src/runtime/trace.ts @@ -348,7 +348,7 @@ class TraceRecorderImpl implements TraceRecorder { // using a binary search over the already sorted traces. const insertionIndex = (() => { var low = 0 - var high = this.bestTraces.length - 1 + var high = this.bestTraces.length while (low < high) { // The index of the middle element in the range that remains to be searched From 9562e291ff89b34c67c2c1f5ec1dc5012026ec73 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Thu, 15 Aug 2024 16:36:47 +0200 Subject: [PATCH 3/7] Add comments --- quint/src/runtime/trace.ts | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/quint/src/runtime/trace.ts b/quint/src/runtime/trace.ts index 9939c408f..21ff0ae71 100644 --- a/quint/src/runtime/trace.ts +++ b/quint/src/runtime/trace.ts @@ -329,9 +329,12 @@ class TraceRecorderImpl implements TraceRecorder { const traceWithSeed = { frame: traceToSave, seed: this.runSeed } + // Insert the trace into the list of best traces, + // keeping the list sorted by descending quality. this.insertTraceSortedByQuality(traceWithSeed) - // Remove the worst trace (if there more traces than needed) + // If there are more traces than needed, remove the worst trace, + // ie. the last one, since the traces are sorted by descending quality. if (this.bestTraces.length > this.tracesToStore) { this.bestTraces.pop() } From aabd67d530155b91f2a73b29ba3253bbd8da6b94 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Sat, 17 Aug 2024 12:32:12 +0200 Subject: [PATCH 4/7] Refactor and add tests --- quint/src/runtime/trace.ts | 35 ++--------------------------- quint/src/util.ts | 42 ++++++++++++++++++++++++++++++++++- quint/test/util.test.ts | 45 ++++++++++++++++++++++++++++++++++++-- 3 files changed, 86 insertions(+), 36 deletions(-) diff --git a/quint/src/runtime/trace.ts b/quint/src/runtime/trace.ts index 21ff0ae71..97502a00c 100644 --- a/quint/src/runtime/trace.ts +++ b/quint/src/runtime/trace.ts @@ -16,6 +16,7 @@ import { EvalResult } from './runtime' import { verbosity } from './../verbosity' import { Rng } from './../rng' import { rv } from './impl/runtimeValue' +import { insertSorted } from './../util' /** * A snapshot of how a single operator (e.g., an action) was executed. @@ -341,39 +342,7 @@ class TraceRecorderImpl implements TraceRecorder { } private insertTraceSortedByQuality(trace: Trace) { - if (this.bestTraces.length === 0) { - // This is the first trace, just add it - this.bestTraces.push(trace) - return - } - - // Compute the index where the trace should be inserted, - // using a binary search over the already sorted traces. - const insertionIndex = (() => { - var low = 0 - var high = this.bestTraces.length - - while (low < high) { - // The index of the middle element in the range that remains to be searched - const mid = (low + high) >>> 1 // Math.floor((low + high) / 2) - - // Compare the trace to insert with the trace at the middle index - if (compareTracesByQuality(trace, this.bestTraces[mid]) < 0) { - // The trace to insert is better than the trace at the middle index, - // so we continue searching in the left half of the range - high = mid - } else { - // The trace to insert is worse than the trace at the middle index, - // so we continue searching in the right half of the range - low = mid + 1 - } - } - - return low - })() - - // Insert the trace at the computed index - this.bestTraces.splice(insertionIndex, 0, trace) + insertSorted(this.bestTraces, trace, compareTracesByQuality) } // create a bottom frame, which encodes the whole trace diff --git a/quint/src/util.ts b/quint/src/util.ts index f57dcec2b..76fdc1c8e 100644 --- a/quint/src/util.ts +++ b/quint/src/util.ts @@ -50,7 +50,7 @@ export function zip(a: A[], b: B[]): [A, B][] { * otherwise, it is `none` * * This is like `Array.prototype.find`, except that it works on any iterable and - * enables trasforming the found value. + * enables transforming the found value. * * Example: * @@ -68,3 +68,43 @@ export function findMap(xs: Iterable, f: (x: X) => Maybe): Maybe } return none() } + +// Insert an item into an array sorted in ascending order by the given comparator. +export function insertSorted(array: A[], item: A, cmp: (a: A, b: A) => number): void { + if (array.length === 0) { + array.push(item) + return + } + + const index = findInsertionIndex(array, x => cmp(x, item) > 0) + array.splice(index, 0, item) +} + +/** Find the `index` in `array` where the predicate `pred(array[index])` is true, + * but `pred(array[index+1])` is false. + * + * Important: The array must be sorted in ascending order. + * + * Implements a binary search with complexity: O(log n) + * + * This function is not exported as it is only meant to be used internally by `insertSorted`. + */ +function findInsertionIndex(array: A[], pred: (a: A) => boolean): number { + var low = 0 + var high = array.length + + while (low < high) { + // Integer version of `Math.floor((low + high) / 2)` + const mid = (low + high) >>> 1 + + if (pred(array[mid])) { + // The element at mid satisfies the predicate, so we need to search to the left + high = mid + } else { + // The element at mid does not satisfy the predicate, so we need to search to the right + low = mid + 1 + } + } + + return low +} diff --git a/quint/test/util.test.ts b/quint/test/util.test.ts index eda8bbfaa..6313d8eec 100644 --- a/quint/test/util.test.ts +++ b/quint/test/util.test.ts @@ -3,14 +3,14 @@ import { describe, it } from 'mocha' import { just, none } from '@sweet-monads/maybe' -import { findMap } from '../src/util' +import { findMap, insertSorted } from '../src/util' describe('findMap', () => { it('is none on empty iterable', () => { assert(findMap(new Map().values(), _ => just(42)).isNone(), 'should be none on empty iterable') }) - it('is `just` when a vaule can be found', () => { + it('is `just` when a value can be found', () => { const actual = findMap( new Map([ ['a', 1], @@ -36,3 +36,44 @@ describe('findMap', () => { assert(result.isNone(), 'should be none') }) }) + +describe('insertSorted', () => { + it('can insert into empty array', () => { + const array: number[] = [] + insertSorted(array, 42, (a, b) => a - b) + assert.deepEqual([42], array) + }) + + it('can insert into sorted array', () => { + const array = [1, 3, 5] + insertSorted(array, 2, (a, b) => a - b) + assert.deepEqual([1, 2, 3, 5], array) + }) + + it('can insert at the beginning of the array', () => { + const array = [2, 3, 4] + insertSorted(array, 1, (a, b) => a - b) + assert.deepEqual([1, 2, 3, 4], array) + }) + + it('can insert at the end of the array', () => { + const array = [1, 2, 3] + insertSorted(array, 4, (a, b) => a - b) + assert.deepEqual([1, 2, 3, 4], array) + }) + + it('can insert at the middle of the array', () => { + const array = [1, 3, 4] + insertSorted(array, 2, (a, b) => a - b) + assert.deepEqual([1, 2, 3, 4], array) + }) + + it('can sort an array of numbers', () => { + const array = [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5] + var sorted: number[] = [] + for (const n of array) { + insertSorted(sorted, n, (a, b) => a - b) + } + assert.deepEqual([1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9], sorted) + }) +}) From 1985fefbf95d6c324f6efcb68d2bad3b1a0558e1 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Mon, 19 Aug 2024 16:04:23 +0200 Subject: [PATCH 5/7] Fix doc comment --- quint/src/util.ts | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/quint/src/util.ts b/quint/src/util.ts index 76fdc1c8e..370d1a694 100644 --- a/quint/src/util.ts +++ b/quint/src/util.ts @@ -80,8 +80,7 @@ export function insertSorted(array: A[], item: A, cmp: (a: A, b: A) => number array.splice(index, 0, item) } -/** Find the `index` in `array` where the predicate `pred(array[index])` is true, - * but `pred(array[index+1])` is false. +/** Find the `index` in `array` where the predicate `pred(array[index])` is true. * * Important: The array must be sorted in ascending order. * From feece6aee2af03d62606a98c3937d205364edbe0 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Mon, 19 Aug 2024 16:09:21 +0200 Subject: [PATCH 6/7] Fix another doc comment --- quint/src/util.ts | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/quint/src/util.ts b/quint/src/util.ts index 370d1a694..d9137f0ce 100644 --- a/quint/src/util.ts +++ b/quint/src/util.ts @@ -69,7 +69,12 @@ export function findMap(xs: Iterable, f: (x: X) => Maybe): Maybe return none() } -// Insert an item into an array sorted in ascending order by the given comparator. +/** Insert an item into an array sorted in ascending order by the given comparator. + * + * Important: The array must be sorted in ascending order. + * + * Complexity: O(log n) + */ export function insertSorted(array: A[], item: A, cmp: (a: A, b: A) => number): void { if (array.length === 0) { array.push(item) From cbb78a2096de856357e33ffe256831d439c783c5 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Mon, 19 Aug 2024 16:31:52 +0200 Subject: [PATCH 7/7] Update doc comment according to code review Co-authored-by: Gabriela Moreira --- quint/src/util.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/quint/src/util.ts b/quint/src/util.ts index d9137f0ce..2ce0caf95 100644 --- a/quint/src/util.ts +++ b/quint/src/util.ts @@ -85,7 +85,7 @@ export function insertSorted(array: A[], item: A, cmp: (a: A, b: A) => number array.splice(index, 0, item) } -/** Find the `index` in `array` where the predicate `pred(array[index])` is true. +/** Find the first `index` in `array` where the predicate `pred(array[index])` is true. * * Important: The array must be sorted in ascending order. *