From fd9be4a4c93587c453509ff5d0b269eb321680a2 Mon Sep 17 00:00:00 2001 From: dbera Date: Tue, 11 Aug 2026 19:31:16 +0200 Subject: [PATCH 1/3] Add any-witness path search strategy --- frontend/src/App.css | 4 +- frontend/src/App.tsx | 47 +++++++++++++++--- frontend/src/graph/graphJson.ts | 15 +++++- frontend/src/graph/pathSearch.ts | 85 +++++++++++++++++++++++++++++--- 4 files changed, 135 insertions(+), 16 deletions(-) diff --git a/frontend/src/App.css b/frontend/src/App.css index 310aa3f..cbf4e1f 100644 --- a/frontend/src/App.css +++ b/frontend/src/App.css @@ -722,8 +722,8 @@ body.resizing-side-panel canvas { .path-search-form { display: grid; gap: 8px; } .path-search-form > label, .path-search-number-row label { color: #475569; font-size: 12px; font-weight: 700; } -.path-search-form input { width: 100%; min-width: 0; padding: 8px 10px; border: 1px solid #cbd5e1; border-radius: 7px; outline: none; } -.path-search-form input:focus { border-color: #2563eb; box-shadow: 0 0 0 3px rgba(37, 99, 235, 0.13); } +.path-search-form input, .path-search-form select { width: 100%; min-width: 0; padding: 8px 10px; border: 1px solid #cbd5e1; border-radius: 7px; outline: none; } +.path-search-form input:focus, .path-search-form select:focus { border-color: #2563eb; box-shadow: 0 0 0 3px rgba(37, 99, 235, 0.13); } .path-search-number-row { display: grid; grid-template-columns: 1fr 1fr; gap: 10px; margin-top: 4px; } .path-search-number-row > div { display: grid; gap: 6px; } .path-search-status { margin-top: 16px; color: #475569; } diff --git a/frontend/src/App.tsx b/frontend/src/App.tsx index dd7a947..0e0cec2 100644 --- a/frontend/src/App.tsx +++ b/frontend/src/App.tsx @@ -38,7 +38,7 @@ import { } from "./graph/graphJson"; import { useGraphAnalysis } from "./graph/useGraphAnalysis"; import { usePathSearch } from "./graph/usePathSearch"; -import type { BoundedPath, ConstraintExplanationEvent } from "./graph/pathSearch"; +import type { BoundedPath, ConstraintExplanationEvent, PathSearchStrategy } from "./graph/pathSearch"; import type { StronglyConnectedComponent } from "./graph/graphAnalysis"; import { buildTransitionCatalogue } from "./graph/transitionCatalog"; import { buildTransitionDataCatalogue } from "./graph/transitionDataCatalogue"; @@ -145,6 +145,7 @@ function App() { const [pathSearchSource, setPathSearchSource] = useState(""); const [pathSearchTarget, setPathSearchTarget] = useState(""); const [requestedPathCount, setRequestedPathCount] = useState(5); + const [pathSearchStrategy, setPathSearchStrategy] = useState("shortest"); const [maximumVisitsPerState, setMaximumVisitsPerState] = useState(1); const [requireConstraintExercise, setRequireConstraintExercise] = useState(true); const [declareConstraints, setDeclareConstraints] = useState([]); @@ -666,11 +667,12 @@ function App() { const targetNodeId = pathSearchTarget.trim(); return { sourceNodeId, + strategy: pathSearchStrategy, endpointMode: targetNodeId ? "specific-target" : "constraint-satisfaction", ...(targetNodeId ? { targetNodeId } : {}), - requestedPathCount, + requestedPathCount: pathSearchStrategy === "any-witness" ? 1 : requestedPathCount, maximumVisitsPerState, requireConstraintExercise, }; @@ -992,18 +994,30 @@ function App() { outputs: edge.outputs, })), sourceNodeId, + strategy: pathSearchStrategy, ...(targetNodeId ? { targetNodeId, endpointMode: "specific-target" as const } : { endpointMode: "constraint-satisfaction" as const }), - requestedPathCount, + requestedPathCount: + pathSearchStrategy === "any-witness" ? 1 : requestedPathCount, maximumVisitsPerState, requireConstraintExercise, constraints: { declare: declareConstraints }, }); + const effectiveRequestedPathCount = + pathSearchStrategy === "any-witness" ? 1 : requestedPathCount; setStatus( targetNodeId - ? `Searching for up to ${requestedPathCount} paths from ${sourceNodeId} to ${targetNodeId}` - : `Searching for up to ${requestedPathCount} constraint-satisfying paths from ${sourceNodeId}`, + ? `Searching for ${ + pathSearchStrategy === "any-witness" + ? "any satisfying path" + : `up to ${effectiveRequestedPathCount} paths` + } from ${sourceNodeId} to ${targetNodeId}` + : `Searching for ${ + pathSearchStrategy === "any-witness" + ? "any constraint-satisfying path" + : `up to ${effectiveRequestedPathCount} constraint-satisfying paths` + } from ${sourceNodeId}`, ); } @@ -1155,6 +1169,7 @@ function App() { setPathSearchSource(importedPathSearch?.sourceNodeId ?? defaultPathState); setPathSearchTarget(importedPathSearch?.targetNodeId ?? ""); setRequestedPathCount(importedPathSearch?.requestedPathCount ?? 5); + setPathSearchStrategy(importedPathSearch?.strategy ?? "shortest"); setMaximumVisitsPerState( importedPathSearch?.maximumVisitsPerState ?? 1, ); @@ -2333,6 +2348,24 @@ function App() { ) : ( <>
+ + +

+ {pathSearchStrategy === "any-witness" + ? "Returns the first satisfying path found; it is not guaranteed to be shortest." + : "Returns paths in deterministic shortest-first order."} +

{ invalidatePathSearchResults(); setPathSearchSource(event.target.value); }} disabled={pathSearch.status === "running"} /> @@ -2371,8 +2404,8 @@ function App() {

- - { invalidatePathSearchResults(); setRequestedPathCount(Math.max(1, Number.parseInt(event.target.value, 10) || 1)); }} disabled={pathSearch.status === "running"} /> + + { invalidatePathSearchResults(); setRequestedPathCount(Math.max(1, Number.parseInt(event.target.value, 10) || 1)); }} disabled={pathSearch.status === "running" || pathSearchStrategy === "any-witness"} />
diff --git a/frontend/src/graph/graphJson.ts b/frontend/src/graph/graphJson.ts index 845b851..7ca8d7e 100644 --- a/frontend/src/graph/graphJson.ts +++ b/frontend/src/graph/graphJson.ts @@ -1,5 +1,5 @@ import type { DeclareConstraint } from "./declareConstraints"; -import type { PathSearchEndpointMode } from "./pathSearch"; +import type { PathSearchEndpointMode, PathSearchStrategy } from "./pathSearch"; import { parseDeclareConstraintsJson } from "./declareConstraintJson"; import { resolvePath, @@ -36,6 +36,7 @@ export interface GraphJsonMetadata { export interface PersistedPathSearchConfiguration { sourceNodeId: string; endpointMode: PathSearchEndpointMode; + strategy?: PathSearchStrategy; targetNodeId?: string; requestedPathCount: number; maximumVisitsPerState: number; @@ -273,6 +274,17 @@ function parsePathSearchConfiguration( 'pathSearch.endpointMode must be either "specific-target" or "constraint-satisfaction".', ); } + const strategyValue = configuration.strategy; + if ( + strategyValue !== undefined && + strategyValue !== "shortest" && + strategyValue !== "any-witness" + ) { + throw new GraphJsonError( + 'pathSearch.strategy must be either "shortest" or "any-witness".', + ); + } + const strategy = strategyValue as PathSearchStrategy | undefined; const nodeIds = new Set(graph.nodes.map((node) => node.id)); if (!nodeIds.has(sourceNodeId)) { throw new GraphJsonError( @@ -298,6 +310,7 @@ function parsePathSearchConfiguration( return { sourceNodeId, endpointMode, + ...(strategy ? { strategy } : {}), ...(targetNodeId ? { targetNodeId } : {}), requestedPathCount: requirePositiveInteger( configuration.requestedPathCount, diff --git a/frontend/src/graph/pathSearch.ts b/frontend/src/graph/pathSearch.ts index 90b193c..cfa0175 100644 --- a/frontend/src/graph/pathSearch.ts +++ b/frontend/src/graph/pathSearch.ts @@ -25,6 +25,8 @@ export type PathConstraints = { declare?: DeclareConstraint[]; }; +export type PathSearchStrategy = "shortest" | "any-witness"; + export type PathSearchEndpointMode = | "specific-target" | "constraint-satisfaction"; @@ -35,6 +37,7 @@ export type PathSearchInput = { sourceNodeId: string; targetNodeId?: string; endpointMode?: PathSearchEndpointMode; + strategy?: PathSearchStrategy; requireConstraintExercise?: boolean; requestedPathCount: number; maximumVisitsPerState: number; @@ -108,6 +111,9 @@ type SearchCandidate = { monitorEntries: MonitorSetEntry[]; exercisedConstraintIds: ReadonlySet; insertionSequence: number; + acceptingConstraintCount?: number; + exercisedConstraintCount?: number; + advancedMonitorCount?: number; }; const DEFAULT_MAXIMUM_EXPANDED_CANDIDATES = 1_000_000; @@ -116,6 +122,14 @@ const DEFAULT_MAXIMUM_QUEUED_CANDIDATES = 100_000; class CandidateMinHeap { private readonly items: SearchCandidate[] = []; + private readonly higherPriority: (left: SearchCandidate, right: SearchCandidate) => boolean; + + public constructor( + higherPriority: (left: SearchCandidate, right: SearchCandidate) => boolean, + ) { + this.higherPriority = higherPriority; + } + public get size(): number { return this.items.length; } @@ -147,7 +161,7 @@ class CandidateMinHeap { while (index > 0) { const parentIndex = Math.floor((index - 1) / 2); - if (!hasHigherPriority(this.items[index], this.items[parentIndex])) { + if (!this.higherPriority(this.items[index], this.items[parentIndex])) { return; } @@ -167,14 +181,14 @@ class CandidateMinHeap { if ( leftIndex < this.items.length && - hasHigherPriority(this.items[leftIndex], this.items[bestIndex]) + this.higherPriority(this.items[leftIndex], this.items[bestIndex]) ) { bestIndex = leftIndex; } if ( rightIndex < this.items.length && - hasHigherPriority(this.items[rightIndex], this.items[bestIndex]) + this.higherPriority(this.items[rightIndex], this.items[bestIndex]) ) { bestIndex = rightIndex; } @@ -190,7 +204,7 @@ class CandidateMinHeap { } } -function hasHigherPriority( +function hasShortestPriority( left: SearchCandidate, right: SearchCandidate, ): boolean { @@ -205,6 +219,48 @@ function hasHigherPriority( return left.insertionSequence < right.insertionSequence; } +function hasAnyWitnessPriority( + left: SearchCandidate, + right: SearchCandidate, +): boolean { + const progressKeys: (keyof SearchCandidate)[] = [ + "acceptingConstraintCount", + "exercisedConstraintCount", + "advancedMonitorCount", + ]; + + for (const key of progressKeys) { + const leftValue = (left[key] as number | undefined) ?? 0; + const rightValue = (right[key] as number | undefined) ?? 0; + if (leftValue !== rightValue) return leftValue > rightValue; + } + + if (left.depth !== right.depth) return left.depth < right.depth; + return left.insertionSequence < right.insertionSequence; +} + +function getAnyWitnessProgress( + entries: readonly MonitorSetEntry[], + initialStateKeys: readonly string[], + exercisedConstraintIds: ReadonlySet, +) { + let acceptingConstraintCount = 0; + let advancedMonitorCount = 0; + + entries.forEach((entry, index) => { + if (entry.monitor.status(entry.state).accepting) acceptingConstraintCount += 1; + if (entry.monitor.stateKey(entry.state) !== initialStateKeys[index]) { + advancedMonitorCount += 1; + } + }); + + return { + acceptingConstraintCount, + exercisedConstraintCount: exercisedConstraintIds.size, + advancedMonitorCount, + }; +} + function buildTopology(input: PathSearchInput): NormalizedTopology { const nodeIds: string[] = []; const knownNodeIds = new Set(); @@ -632,6 +688,11 @@ export function findKShortestBoundedPaths( const edgesById = new Map(input.edges.map((edge) => [edge.id, edge])); const initialMonitorEntries = createMonitorSet(compiledConstraints); const requireConstraintExercise = input.requireConstraintExercise ?? true; + const strategy = input.strategy ?? "shortest"; + const effectiveRequestedPathCount = strategy === "any-witness" ? 1 : input.requestedPathCount; + const initialMonitorStateKeys = initialMonitorEntries.map((entry) => + entry.monitor.stateKey(entry.state), + ); if ( endpointMode === "constraint-satisfaction" && @@ -642,7 +703,9 @@ export function findKShortestBoundedPaths( ); } - const queue = new CandidateMinHeap(); + const queue = new CandidateMinHeap( + strategy === "any-witness" ? hasAnyWitnessPriority : hasShortestPriority, + ); let nextInsertionSequence = 1; let expandedCandidateCount = 0; let peakQueuedCandidateCount = 1; @@ -661,6 +724,9 @@ export function findKShortestBoundedPaths( monitorEntries: initialMonitorEntries, exercisedConstraintIds: new Set(), insertionSequence: 0, + ...(strategy === "any-witness" + ? getAnyWitnessProgress(initialMonitorEntries, initialMonitorStateKeys, new Set()) + : {}), }); const paths: BoundedPath[] = []; @@ -791,6 +857,13 @@ export function findKShortestBoundedPaths( monitorEntries: nextMonitorEntries, exercisedConstraintIds: nextExercisedConstraintIds, insertionSequence: nextInsertionSequence, + ...(strategy === "any-witness" + ? getAnyWitnessProgress( + nextMonitorEntries, + initialMonitorStateKeys, + nextExercisedConstraintIds, + ) + : {}), }); nextInsertionSequence += 1; peakQueuedCandidateCount = Math.max( @@ -804,7 +877,7 @@ export function findKShortestBoundedPaths( } } - const requestedCountReached = paths.length >= input.requestedPathCount; + const requestedCountReached = paths.length >= effectiveRequestedPathCount; const exhausted = !requestedCountReached && !resourceLimitReached && From 2b37d931acd4b3e7da54f1fd652fde0fbcfee442 Mon Sep 17 00:00:00 2001 From: dbera Date: Tue, 11 Aug 2026 23:46:32 +0200 Subject: [PATCH 2/3] Allow multiple any-witness paths --- frontend/src/App.tsx | 34 +++-- frontend/src/graph/pathSearch.test.ts | 200 ++++++++++++++++++++++++++ frontend/src/graph/pathSearch.ts | 7 +- 3 files changed, 220 insertions(+), 21 deletions(-) diff --git a/frontend/src/App.tsx b/frontend/src/App.tsx index 0e0cec2..bd49541 100644 --- a/frontend/src/App.tsx +++ b/frontend/src/App.tsx @@ -672,7 +672,8 @@ function App() { ? "specific-target" : "constraint-satisfaction", ...(targetNodeId ? { targetNodeId } : {}), - requestedPathCount: pathSearchStrategy === "any-witness" ? 1 : requestedPathCount, + // requestedPathCount: pathSearchStrategy === "any-witness" ? 1 : requestedPathCount, + requestedPathCount, maximumVisitsPerState, requireConstraintExercise, }; @@ -998,26 +999,23 @@ function App() { ...(targetNodeId ? { targetNodeId, endpointMode: "specific-target" as const } : { endpointMode: "constraint-satisfaction" as const }), - requestedPathCount: - pathSearchStrategy === "any-witness" ? 1 : requestedPathCount, + // requestedPathCount: + // pathSearchStrategy === "any-witness" ? 1 : requestedPathCount, + requestedPathCount, maximumVisitsPerState, requireConstraintExercise, constraints: { declare: declareConstraints }, }); - const effectiveRequestedPathCount = - pathSearchStrategy === "any-witness" ? 1 : requestedPathCount; + // const effectiveRequestedPathCount = + // pathSearchStrategy === "any-witness" ? 1 : requestedPathCount; setStatus( targetNodeId - ? `Searching for ${ - pathSearchStrategy === "any-witness" - ? "any satisfying path" - : `up to ${effectiveRequestedPathCount} paths` - } from ${sourceNodeId} to ${targetNodeId}` - : `Searching for ${ - pathSearchStrategy === "any-witness" - ? "any constraint-satisfying path" - : `up to ${effectiveRequestedPathCount} constraint-satisfying paths` - } from ${sourceNodeId}`, + ? pathSearchStrategy === "any-witness" + ? `Searching for up to ${requestedPathCount} witnesses from ${sourceNodeId} to ${targetNodeId} in heuristic discovery order` + : `Searching for up to ${requestedPathCount} shortest paths from ${sourceNodeId} to ${targetNodeId}` + : pathSearchStrategy === "any-witness" + ? `Searching for up to ${requestedPathCount} constraint-satisfying witnesses from ${sourceNodeId} in heuristic discovery order` + : `Searching for up to ${requestedPathCount} shortest constraint-satisfying paths from ${sourceNodeId}`, ); } @@ -2363,7 +2361,7 @@ function App() {

{pathSearchStrategy === "any-witness" - ? "Returns the first satisfying path found; it is not guaranteed to be shortest." + ? "Returns up to the requested number of satisfying paths in heuristic discovery order. Results are not guaranteed to be shortest." : "Returns paths in deterministic shortest-first order."}

@@ -2404,8 +2402,8 @@ function App() {

- - { invalidatePathSearchResults(); setRequestedPathCount(Math.max(1, Number.parseInt(event.target.value, 10) || 1)); }} disabled={pathSearch.status === "running" || pathSearchStrategy === "any-witness"} /> + + { invalidatePathSearchResults(); setRequestedPathCount(Math.max(1, Number.parseInt(event.target.value, 10) || 1)); }} disabled={pathSearch.status === "running"} />
diff --git a/frontend/src/graph/pathSearch.test.ts b/frontend/src/graph/pathSearch.test.ts index 1aeaa02..dbd5412 100644 --- a/frontend/src/graph/pathSearch.test.ts +++ b/frontend/src/graph/pathSearch.test.ts @@ -957,4 +957,204 @@ describe("findKShortestBoundedPaths", () => { expect(result.paths.map((path) => path.edgeIds)).toEqual([["a", "x", "b"]]); }); + + describe("any-witness multiple-path and loop behavior", () => { + const atLeastOneA = { + id: "at-least-one-a", + template: "at-least" as const, + enabled: true, + count: 1, + activation: groupForTest("A"), + }; + + it("honors the requested path count in any-witness mode", () => { + const result = findKShortestBoundedPaths({ + nodeIds: ["source", "one", "two", "three", "four"], + edges: [ + { id: "a-1", source: "source", target: "one", transition: "A" }, + { id: "a-2", source: "source", target: "two", transition: "A" }, + { id: "a-3", source: "source", target: "three", transition: "A" }, + { id: "a-4", source: "source", target: "four", transition: "A" }, + ], + sourceNodeId: "source", + endpointMode: "constraint-satisfaction", + strategy: "any-witness", + requestedPathCount: 3, + maximumVisitsPerState: 1, + constraints: { declare: [atLeastOneA] }, + }); + + expect(result.paths.map((path) => path.edgeIds)).toEqual([ + ["a-1"], + ["a-2"], + ["a-3"], + ]); + expect(result.stopReason).toBe("requested-count-reached"); + expect(result.exhausted).toBe(false); + }); + + it("returns fewer witnesses when the bounded search space is exhausted", () => { + const result = findKShortestBoundedPaths({ + nodeIds: ["source", "one", "two"], + edges: [ + { id: "a-1", source: "source", target: "one", transition: "A" }, + { id: "a-2", source: "source", target: "two", transition: "A" }, + ], + sourceNodeId: "source", + endpointMode: "constraint-satisfaction", + strategy: "any-witness", + requestedPathCount: 5, + maximumVisitsPerState: 1, + constraints: { declare: [atLeastOneA] }, + }); + + expect(result.paths.map((path) => path.edgeIds)).toEqual([ + ["a-1"], + ["a-2"], + ]); + expect(result.stopReason).toBe("exhausted"); + expect(result.exhausted).toBe(true); + }); + + it("keeps parallel-edge witnesses distinct by ordered edge ID", () => { + const input: PathSearchInput = { + nodeIds: ["source", "target"], + edges: [ + { id: "a-primary", source: "source", target: "target", transition: "A" }, + { id: "a-alternative", source: "source", target: "target", transition: "A" }, + ], + sourceNodeId: "source", + targetNodeId: "target", + endpointMode: "specific-target", + strategy: "any-witness", + requestedPathCount: 2, + maximumVisitsPerState: 1, + constraints: { declare: [atLeastOneA] }, + }; + + const first = findKShortestBoundedPaths(input); + const second = findKShortestBoundedPaths(input); + + expect(first.paths.map((path) => path.edgeIds)).toEqual([ + ["a-primary"], + ["a-alternative"], + ]); + expect(second).toEqual(first); + }); + + it("rejects a loop-dependent witness when visits per state is one", () => { + const result = findKShortestBoundedPaths({ + nodeIds: ["source", "middle", "target"], + edges: [ + { id: "first-a", source: "source", target: "middle", transition: "A" }, + { id: "return", source: "middle", target: "source", transition: "X" }, + { id: "second-a", source: "source", target: "target", transition: "A" }, + ], + sourceNodeId: "source", + targetNodeId: "target", + endpointMode: "specific-target", + strategy: "any-witness", + requestedPathCount: 1, + maximumVisitsPerState: 1, + constraints: { + declare: [{ + ...atLeastOneA, + id: "at-least-two-a", + count: 2, + }], + }, + }); + + expect(result.paths).toEqual([]); + expect(result.stopReason).toBe("exhausted"); + }); + + it("accepts the same loop-dependent witness when visits per state is two", () => { + const result = findKShortestBoundedPaths({ + nodeIds: ["source", "middle", "target"], + edges: [ + { id: "first-a", source: "source", target: "middle", transition: "A" }, + { id: "return", source: "middle", target: "source", transition: "X" }, + { id: "second-a", source: "source", target: "target", transition: "A" }, + ], + sourceNodeId: "source", + targetNodeId: "target", + endpointMode: "specific-target", + strategy: "any-witness", + requestedPathCount: 1, + maximumVisitsPerState: 2, + constraints: { + declare: [{ + ...atLeastOneA, + id: "at-least-two-a", + count: 2, + }], + }, + }); + + expect(result.paths).toHaveLength(1); + expect(result.paths[0]).toMatchObject({ + startNodeId: "source", + edgeIds: ["first-a", "return", "second-a"], + }); + expect(result.stopReason).toBe("requested-count-reached"); + }); + + it("applies the visit bound to self-loops in any-witness mode", () => { + const baseInput: PathSearchInput = { + nodeIds: ["source", "target"], + edges: [ + { id: "loop-a", source: "source", target: "source", transition: "A" }, + { id: "exit-a", source: "source", target: "target", transition: "A" }, + ], + sourceNodeId: "source", + endpointMode: "constraint-satisfaction", + strategy: "any-witness", + requestedPathCount: 1, + maximumVisitsPerState: 1, + constraints: { + declare: [{ + ...atLeastOneA, + id: "at-least-two-a", + count: 2, + }], + }, + }; + + const loopless = findKShortestBoundedPaths(baseInput); + const oneSelfLoopAllowed = findKShortestBoundedPaths({ + ...baseInput, + maximumVisitsPerState: 2, + }); + + expect(loopless.paths).toEqual([]); + expect(oneSelfLoopAllowed.paths[0]).toMatchObject({ + startNodeId: "source", + endNodeId: "target", + edgeIds: ["loop-a", "exit-a"], + }); + }); + + it("does not change deterministic shortest-first behavior", () => { + const result = findKShortestBoundedPaths( + searchInput( + ["source", "near", "far-1", "far-2", "target"], + [ + { id: "far-start", source: "source", target: "far-1" }, + { id: "far-middle", source: "far-1", target: "far-2" }, + { id: "far-end", source: "far-2", target: "target" }, + { id: "near-start", source: "source", target: "near" }, + { id: "near-end", source: "near", target: "target" }, + ], + { strategy: "shortest", requestedPathCount: 2 }, + ), + ); + + expect(result.paths.map((path) => path.edgeIds)).toEqual([ + ["near-start", "near-end"], + ["far-start", "far-middle", "far-end"], + ]); + }); + }); + }); diff --git a/frontend/src/graph/pathSearch.ts b/frontend/src/graph/pathSearch.ts index cfa0175..c3d52e8 100644 --- a/frontend/src/graph/pathSearch.ts +++ b/frontend/src/graph/pathSearch.ts @@ -116,8 +116,8 @@ type SearchCandidate = { advancedMonitorCount?: number; }; -const DEFAULT_MAXIMUM_EXPANDED_CANDIDATES = 1_000_000; -const DEFAULT_MAXIMUM_QUEUED_CANDIDATES = 100_000; +const DEFAULT_MAXIMUM_EXPANDED_CANDIDATES = 9_000_000; +const DEFAULT_MAXIMUM_QUEUED_CANDIDATES = 900_000; class CandidateMinHeap { private readonly items: SearchCandidate[] = []; @@ -689,7 +689,8 @@ export function findKShortestBoundedPaths( const initialMonitorEntries = createMonitorSet(compiledConstraints); const requireConstraintExercise = input.requireConstraintExercise ?? true; const strategy = input.strategy ?? "shortest"; - const effectiveRequestedPathCount = strategy === "any-witness" ? 1 : input.requestedPathCount; + // const effectiveRequestedPathCount = strategy === "any-witness" ? 1 : input.requestedPathCount; + const effectiveRequestedPathCount = input.requestedPathCount; const initialMonitorStateKeys = initialMonitorEntries.map((entry) => entry.monitor.stateKey(entry.state), ); From 1b786904367f2b76323a19e7a934a47ef9bc5b97 Mon Sep 17 00:00:00 2001 From: dbera Date: Wed, 12 Aug 2026 00:37:06 +0200 Subject: [PATCH 3/3] Updated Documentation --- CHANGELOG.md | 14 +++++++++++- README.md | 61 ++++++++++++++++++++++++++++------------------------ 2 files changed, 46 insertions(+), 29 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ed45f95..249939a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,9 +4,16 @@ All notable changes to LTSVisualizer are documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), and this project follows [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [Unreleased](https://github.com/dbera/LTSVisualizer/compare/v0.5.0...HEAD) +## [Unreleased](https://github.com/dbera/LTSVisualizer/compare/v0.6.0...HEAD) + +## [0.6.0](https://github.com/dbera/LTSVisualizer/compare/v0.5.0...v0.6.0) - 2026-08-10 ### Added +- Added a selectable **Any witness (fast)** strategy alongside the existing deterministic **Shortest paths** strategy. +- Added generic Any-witness candidate prioritization based on accepting constraints, exercised constraints, monitors advanced from their initial state, path depth, and deterministic insertion order. +- Added support for returning up to the user-requested number of Any-witness paths in heuristic discovery order. +- Added persistence and restoration of the selected path-search strategy in complete-graph JSON exports. +- Added focused tests for requested witness counts, bounded-search exhaustion, deterministic results, parallel-edge identity, bounded revisits, loop-dependent witnesses, self-loops, and shortest-strategy regression behavior. - Added structured explanations for accepted Declare-constrained paths, including constraint ID, template, satisfaction summary, exercised or vacuous status, one-based path steps, transition names, and exact edge IDs. - Added expandable **Why this path satisfies the constraints** sections below computed paths. - Added clickable explanation evidence that focuses the corresponding transition and displays its inputs and outputs in the Inspector. @@ -17,6 +24,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), - Added regression tests for explanation payloads, persisted constraints and search settings, standard Alternate semantics, and exercise enforcement in target-specific searches. ### Changed +- Allowed **Number of paths** to remain user-configurable in Any-witness mode instead of forcing a single result. +- Updated constrained path-search help and status text to distinguish shortest-first results from heuristic witness discovery. +- Kept both strategies on the same expanded- and queued-candidate resource safeguards so their search budgets remain directly comparable. - Updated the positive Alternate family to standard two-operand Declare/MP-Declare semantics. - Changed **Alternate response** so unrelated events are allowed between a qualifying activation and correlated target, while another qualifying activation before fulfillment violates the constraint. - Changed **Alternate precedence** so each qualifying target requires a correlated activation since the previous qualifying target. @@ -31,6 +41,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), - Removed **Not alternate response**, **Not alternate precedence**, and **Not alternate succession** because their former specialized interval semantics were not standard Declare/MP-Declare templates. ### Fixed +- Fixed the selected Any-witness strategy not being passed from the Paths UI into the worker search input, which previously caused the search to fall back to shortest-first behavior. +- Fixed Any-witness graph exports forcing the persisted requested path count back to one. - Fixed target-specific searches ignoring the checked **Require constraints to be exercised** option. - Fixed positive Alternate templates rejecting arbitrary configured `between` events instead of only enforcing standard alternation between qualifying activation and target events. - Fixed documentation that described the removed negative Alternate templates and obsolete third Alternate operand. diff --git a/README.md b/README.md index e7ac9e1..7a99d73 100644 --- a/README.md +++ b/README.md @@ -103,12 +103,14 @@ Analysis results are held in browser memory for the currently loaded graph. They ### Bounded alternative path search -- Open the **Paths** tab to compute up to a user-defined number of shortest paths between two states. -- Set **Visits per state** to `1` for loopless paths or to a higher value to allow bounded revisits. +- Open the **Paths** tab and choose **Shortest paths** or **Any witness (fast)**. +- Use **Shortest paths** to compute up to a user-defined number of paths in deterministic shortest-first order. +- Use **Any witness (fast)** to compute up to a user-defined number of satisfying paths in deterministic heuristic discovery order; these paths are not guaranteed to be shortest. +- Any-witness priority is generic and favors candidates with more accepting constraints, more exercised constraints, and more monitors advanced from their initial state before using path length and insertion order as tie-breakers. +- Set **Visits per state** to `1` for loopless paths or to a higher value to allow bounded revisits and self-loops. - Support equal source and target states. The zero-transition path is returned first, and returning cycles may follow when the visit bound permits them. - Treat paths as unique by ordered edge-ID sequence, so parallel transitions remain distinct even when they connect the same states. -- Order results by increasing transition count, with deterministic ordering for equal-length alternatives. -- Use reverse shortest-distance guidance from the target to prioritize reachable alternatives and prune states that cannot reach the target. +- Use reverse shortest-distance guidance from a fixed target for shortest-path search and generic Declare-monitor progress for Any-witness search. - Run searches in an inline Web Worker with cancellation, stale-result protection, errors, reruns, and reset when another graph is loaded. - Stop safely at internal candidate safeguards and report partial results without claiming that no additional paths exist. - Select a result to reuse existing path visualization and JSON and PlantUML exports. @@ -139,7 +141,7 @@ Path-search results are kept in browser memory for the currently loaded graph an - Search either toward a required target state or for a constraint-satisfying path without a fixed target. - Optionally require every applicable enabled constraint to be exercised, excluding paths that satisfy only vacuously. - Apply exercise checking consistently to target-specific and target-free searches. -- Run constrained searches in the existing path-search worker with cancellation, stale-result protection, bounded revisits, deterministic shortest-first results, and parallel-edge identity. +- Run constrained searches in the existing path-search worker with cancellation, stale-result protection, bounded revisits, parallel-edge identity, and a choice between deterministic shortest-first search and deterministic any-witness heuristic discovery. - Use the same constrained-search functionality in hosted and offline `file:///` builds. All enabled constraints must be satisfied by a returned path. Disabling a constraint excludes it from evaluation but keeps it available for later reuse. Vacuous satisfaction remains part of Declare semantics; **Require constraints to be exercised** can be used when returned paths must demonstrate participating constraint events. @@ -204,7 +206,7 @@ Constraint monitors remain authoritative for path pruning and acceptance. Explan Complete-graph JSON exports preserve: - Configured Declare constraints and their enabled state. - Nested transition-data conditions, activation captures, and target correlations. -- Source state and endpoint mode. +- Source state, endpoint mode, and selected search strategy. - Optional target state. - Requested path count and maximum visits per state. - The **Require constraints to be exercised** setting. @@ -515,31 +517,33 @@ For large graphs, worker execution prevents the analysis algorithm from blocking 1. Open the **Paths** tab. 2. Enter source and target state IDs. -3. Choose the requested number of paths. -4. Set **Visits per state** to `1` for loopless paths or higher for bounded revisits. -5. Select **Find paths**. During a running search, the action changes to **Cancel**. -6. Select a result to display it without relaying out its states. -7. Expand **Show transition details** to compare transition names, state pairs, and edge IDs. -8. Select a transition name or edge ID to center and select its edge, or select a state ID to center and select its state. -9. Use **Export .puml** or **Export .json** to export the displayed computed path. -10. Select **Return to graph view** to restore the prior graph context without clearing results. - -Paths are ordered by transition count and are unique by ordered edge IDs. If source and target are equal, the zero-transition path is valid. +3. Select **Shortest paths** for deterministic shortest-first results, or **Any witness (fast)** for heuristic discovery without a shortestness guarantee. +4. Choose the requested number of paths. Both strategies respect this value. +5. Set **Visits per state** to `1` for loopless paths or higher for bounded revisits and self-loops. +6. Select **Find paths**. During a running search, the action changes to **Cancel**. +7. Select a result to display it without relaying out its states. +8. Expand **Show transition details** to compare transition names, state pairs, and edge IDs. +9. Select a transition name or edge ID to center and select its edge, or select a state ID to center and select its state. +10. Use **Export .puml** or **Export .json** to export the displayed computed path. +11. Select **Return to graph view** to restore the prior graph context without clearing results. + +Shortest-path results are ordered by transition count. Any-witness results are ordered by generic constraint-progress priority and are not guaranteed to be shortest. In both strategies, paths are unique by ordered edge IDs. If source and target are equal, the zero-transition path is valid. ### Find Declare-constrained paths 1. Open the **Paths** tab. 2. Enter the source state ID. 3. Enter a target state ID when the path must end at a particular state, or leave the target empty to search for a constraint-satisfying path without a fixed destination. -4. Choose the requested number of paths and set **Visits per state**. -5. In the Declare constraints section, select **Add constraint**. -6. Choose a Declare template and configure its required activation and, where applicable, target transition. -7. For a transition-data predicate, select **Add condition**, choose an input or output field, configure each array-access level, select an operator, and provide a typed value when required. -8. Configure activation captures and target correlation when events must refer to the same data item. -9. Add further conditions or constraints as needed. Conditions within a predicate and enabled constraints in the search are combined conjunctively. -10. Enable **Require constraints to be exercised** when vacuously satisfied paths should be excluded. -11. Select **Find paths**. Invalid or incomplete constraints are reported before search starts. -12. Expand **Why this path satisfies the constraints** to inspect the evidence, or select a result to visualize and export it using the normal computed-path controls. +4. Select **Shortest paths** or **Any witness (fast)**. +5. Choose the requested number of paths and set **Visits per state**. Any-witness mode may find an initial satisfying path much sooner, while requesting additional witnesses can require substantially more search. +6. In the Declare constraints section, select **Add constraint**. +8. Choose a Declare template and configure its required activation and, where applicable, target transition. +8. For a transition-data predicate, select **Add condition**, choose an input or output field, configure each array-access level, select an operator, and provide a typed value when required. +9. Configure activation captures and target correlation when events must refer to the same data item. +10. Add further conditions or constraints as needed. Conditions within a predicate and enabled constraints in the search are combined conjunctively. +11. Enable **Require constraints to be exercised** when vacuously satisfied paths should be excluded. +12. Select **Find paths**. Invalid or incomplete constraints are reported before search starts. +13. Expand **Why this path satisfies the constraints** to inspect the evidence, or select a result to visualize and export it using the normal computed-path controls. Use the enable control to temporarily exclude a constraint while preserving its configuration. Changing a constraint invalidates earlier search results because those results were computed under a different search specification. @@ -765,7 +769,7 @@ npm run build npm run build:offline ``` -The current test suite covers JSON validation and round trips, graph serialization, complete-graph export, manual and computed path selection, loops, repeated states, bounded revisits, source-equals-target paths, self-loops, parallel edges, deterministic shortest-first ordering, reverse-distance pruning, resource safeguards, Declare constraint validation and monitor semantics, standard Alternate semantics, exercise enforcement for targeted and target-free searches, accepted-path explanations, persisted Declare/search configuration, transition-data predicates and correlation, optional-target constrained search, nested and multidimensional array conditions, typed condition values, side-panel state, selected-path export, semantic data, PlantUML path export, terminal-state detection, iterative SCC computation, large synthetic graph topologies, and worker-controller lifecycle behavior. +The current test suite covers JSON validation and round trips, graph serialization, complete-graph export, manual and computed path selection, loops, repeated states, bounded revisits, source-equals-target paths, self-loops, parallel edges, deterministic shortest-first ordering, generic any-witness ordering, multiple witnesses, requested-count handling, reverse-distance pruning, resource safeguards, Declare constraint validation and monitor semantics, standard Alternate semantics, exercise enforcement for targeted and target-free searches, accepted-path explanations, persisted Declare/search configuration, transition-data predicates and correlation, optional-target constrained search, nested and multidimensional array conditions, typed condition values, side-panel state, selected-path export, semantic data, PlantUML path export, terminal-state detection, iterative SCC computation, large synthetic graph topologies, and worker-controller lifecycle behavior. ## Build targets @@ -843,8 +847,8 @@ git status 7. Create and push an annotated version tag: ```powershell -git tag -a v0.4.0 -m "LTSVisualizer 0.4.0" -git push origin v0.4.0 +git tag -a v0.6.0 -m "LTSVisualizer 0.6.0" +git push origin v0.6.0 ``` The tag triggers the offline HTML release workflow and publishes `LTSVisualizer.html` and `SHA256SUMS.txt` to the corresponding GitHub Release. @@ -858,6 +862,7 @@ The tag triggers the offline HTML release workflow and publishes `LTSVisualizer. - Terminal states are reported topologically and are not classified as successful completions or definite deadlocks. - Graph analysis uses a worker and is user-triggered, but very large graphs still require additional browser memory for topology transfer and analysis results. - Bounded path search is user-triggered and uses a worker, but highly connected graphs can still reach internal candidate safeguards before every requested alternative is found. Partial results are reported and additional valid paths may exist. +- Any-witness results are heuristic discoveries rather than shortest-path guarantees. Requesting additional witnesses can substantially increase search time and memory use. - Cancelling path search terminates its worker immediately; partial paths found before cancellation are not retained. - Declare constraints are evaluated during bounded path search; configured visit and result limits still determine the explored search space. - LTSVisualizer currently implements control-flow and data-aware Declare semantics, but not MP-Declare quantitative time intervals.