From d946a4b0f1020b185151f58d00056f4d3ddb76ff Mon Sep 17 00:00:00 2001 From: dbera Date: Sun, 9 Aug 2026 11:02:31 +0200 Subject: [PATCH 1/4] feat: support persistable Declare constraints --- frontend/src/App.tsx | 20 +- .../src/graph/declareConstraintJson.test.ts | 109 ++++ frontend/src/graph/declareConstraintJson.ts | 509 ++++++++++++++++++ frontend/src/graph/graphJson.test.ts | 56 ++ frontend/src/graph/graphJson.ts | 24 +- 5 files changed, 710 insertions(+), 8 deletions(-) create mode 100644 frontend/src/graph/declareConstraintJson.test.ts create mode 100644 frontend/src/graph/declareConstraintJson.ts diff --git a/frontend/src/App.tsx b/frontend/src/App.tsx index 1ed0c42..61ffecd 100644 --- a/frontend/src/App.tsx +++ b/frontend/src/App.tsx @@ -672,9 +672,11 @@ function App() { const safeName = sourceName .replace(/[^a-zA-Z0-9._-]+/g, "-") .replace(/^-+|-+$/g, "") || "graph"; - const document = createGraphJsonDocument(graph, { - title: sourceName, - }); + const document = createGraphJsonDocument( + graph, + { title: sourceName }, + declareConstraints, + ); const exportFileName = `${safeName}.json`; downloadTextFile( @@ -722,9 +724,14 @@ function App() { try { const resolved = resolvePath(graph, path); - const document = createSelectedPathJsonDocument(graph, path, { - title: `Selected path ${resolved.startNodeId} to ${resolved.endNodeId}`, - }); + const document = createSelectedPathJsonDocument( + graph, + path, + { + title: `Selected path ${resolved.startNodeId} to ${resolved.endNodeId}`, + }, + declareConstraints, + ); const fileName = `LTSVisualizer-path-${resolved.startNodeId}-to-${resolved.endNodeId}.json`; downloadTextFile( serializeGraphJson(document), @@ -1113,6 +1120,7 @@ function App() { const parsed = parseGraphJsonText(await file.text()); const graph: GraphData = parsed.graph; const importedPath = parsed.selectedPath; + setDeclareConstraints(parsed.declareConstraints); graphRef.current = graph; setGraphLoaded(true); diff --git a/frontend/src/graph/declareConstraintJson.test.ts b/frontend/src/graph/declareConstraintJson.test.ts new file mode 100644 index 0000000..44ccf37 --- /dev/null +++ b/frontend/src/graph/declareConstraintJson.test.ts @@ -0,0 +1,109 @@ +import { describe, expect, it } from "vitest"; +import { parseDeclareConstraintsJson } from "./declareConstraintJson"; + +describe("parseDeclareConstraintsJson", () => { + it("parses nested conditions, captures, and correlation data", () => { + const value = [ + { + id: "same-request-completes", + template: "response", + enabled: true, + activation: { + relation: "or", + predicates: [ + { + transition: { operator: "equals", value: "SubmitRequest" }, + condition: { + type: "source", + source: "inputs", + condition: { + type: "comparison", + path: ["request", "priority"], + operator: ">=", + value: 5, + }, + }, + captures: [ + { alias: "request_id", source: "inputs", path: ["request", "id"] }, + ], + }, + ], + }, + target: { + relation: "or", + predicates: [ + { transition: { operator: "equals", value: "CompleteRequest" } }, + ], + }, + correlation: { + type: "contains-item", + source: "outputs", + path: ["completed"], + condition: { + type: "comparison", + left: { kind: "item", path: ["id"] }, + operator: "=", + right: { kind: "activation", alias: "request_id" }, + }, + }, + }, + ]; + + expect(parseDeclareConstraintsJson(value)).toEqual(value); + }); + + it("keeps structurally valid editable drafts", () => { + const draft = [ + { + id: "draft-response", + template: "response", + enabled: false, + activation: { relation: "or", predicates: [{}] }, + }, + ]; + expect(parseDeclareConstraintsJson(draft)).toEqual(draft); + }); + + it("rejects unknown templates and malformed nested values", () => { + expect(() => + parseDeclareConstraintsJson([ + { id: "bad", template: "unknown", enabled: true }, + ]), + ).toThrow(/unknown Declare template/); + + expect(() => + parseDeclareConstraintsJson([ + { + id: "bad-path", + template: "response", + enabled: true, + activation: { + relation: "or", + predicates: [ + { + condition: { + type: "source", + source: "inputs", + condition: { + type: "comparison", + path: ["items", -1], + operator: "exists", + }, + }, + }, + ], + }, + }, + ]), + ).toThrow(/non-negative integer/); + }); + + it("rejects duplicate constraint IDs", () => { + expect(() => + parseDeclareConstraintsJson([ + { id: "duplicate", template: "init", enabled: true }, + { id: "duplicate", template: "end", enabled: false }, + ]), + ).toThrow(/Duplicate Declare constraint ID/); + }); +}); diff --git a/frontend/src/graph/declareConstraintJson.ts b/frontend/src/graph/declareConstraintJson.ts new file mode 100644 index 0000000..01682a6 --- /dev/null +++ b/frontend/src/graph/declareConstraintJson.ts @@ -0,0 +1,509 @@ +import { + DECLARE_TEMPLATE_DEFINITIONS, + type ActivityRelation, + type DeclareConstraint, + type DeclarePredicate, + type DeclarePredicateGroup, + type DeclareTemplateId, + type TransitionNameMatcher, +} from "./declareConstraints"; +import type { + ComparisonOperator, + DataPathSegment, + DataSource, + JsonValue, + TransitionCondition, + ValueCondition, +} from "./transitionConditions"; +import type { + CaptureDefinition, + CorrelationCondition, + CorrelationValueReference, +} from "./transitionCorrelation"; + +export class DeclareConstraintJsonError extends Error { + constructor(message: string) { + super(message); + this.name = "DeclareConstraintJsonError"; + } +} + +type JsonObject = Record; + +const TEMPLATE_IDS = new Set( + DECLARE_TEMPLATE_DEFINITIONS.map((definition) => definition.id), +); +const COMPARISON_OPERATORS = new Set([ + "=", + "!=", + "<", + "<=", + ">", + ">=", + "exists", + "does-not-exist", +]); +const CORRELATION_COMPARISON_OPERATORS = new Set([ + "=", + "!=", + "<", + "<=", + ">", + ">=", +]); + +function isObject(value: unknown): value is JsonObject { + return typeof value === "object" && value !== null && !Array.isArray(value); +} + +function requireObject(value: unknown, location: string): JsonObject { + if (!isObject(value)) { + throw new DeclareConstraintJsonError(`${location} must be a JSON object.`); + } + return value; +} + +function requireArray(value: unknown, location: string): unknown[] { + if (!Array.isArray(value)) { + throw new DeclareConstraintJsonError(`${location} must be an array.`); + } + return value; +} + +function requireString(value: unknown, location: string): string { + if (typeof value !== "string") { + throw new DeclareConstraintJsonError(`${location} must be a string.`); + } + return value; +} + +function requireNonEmptyString(value: unknown, location: string): string { + const result = requireString(value, location); + if (result.length === 0) { + throw new DeclareConstraintJsonError(`${location} must not be empty.`); + } + return result; +} + +function requireBoolean(value: unknown, location: string): boolean { + if (typeof value !== "boolean") { + throw new DeclareConstraintJsonError(`${location} must be a boolean.`); + } + return value; +} + +function parseAndOr(value: unknown, location: string): "and" | "or" { + if (value !== "and" && value !== "or") { + throw new DeclareConstraintJsonError(`${location} must be "and" or "or".`); + } + return value; +} + +function parseDataSource(value: unknown, location: string): DataSource { + if (value !== "inputs" && value !== "outputs") { + throw new DeclareConstraintJsonError( + `${location} must be "inputs" or "outputs".`, + ); + } + return value; +} + +function parseDataPath(value: unknown, location: string): DataPathSegment[] { + return requireArray(value, location).map((segment, index) => { + if (typeof segment === "string") return segment; + if (typeof segment === "number" && Number.isInteger(segment) && segment >= 0) { + return segment; + } + throw new DeclareConstraintJsonError( + `${location}[${index}] must be a string or a non-negative integer.`, + ); + }); +} + +function parseJsonValue(value: unknown, location: string): JsonValue { + if ( + value === null || + typeof value === "string" || + typeof value === "boolean" + ) { + return value; + } + if (typeof value === "number") { + if (!Number.isFinite(value)) { + throw new DeclareConstraintJsonError(`${location} must be a finite number.`); + } + return value; + } + if (Array.isArray(value)) { + return value.map((item, index) => parseJsonValue(item, `${location}[${index}]`)); + } + if (isObject(value)) { + return Object.fromEntries( + Object.entries(value).map(([key, item]) => [ + key, + parseJsonValue(item, `${location}.${key}`), + ]), + ); + } + throw new DeclareConstraintJsonError(`${location} must contain JSON data.`); +} + +function parseJsonObjectValue( + value: unknown, + location: string, +): { [key: string]: JsonValue } { + const object = requireObject(value, location); + return Object.fromEntries( + Object.entries(object).map(([key, item]) => [ + key, + parseJsonValue(item, `${location}.${key}`), + ]), + ); +} + +function parseComparisonOperator( + value: unknown, + location: string, +): ComparisonOperator { + if (typeof value !== "string" || !COMPARISON_OPERATORS.has(value)) { + throw new DeclareConstraintJsonError( + `${location} must be a supported comparison operator.`, + ); + } + return value as ComparisonOperator; +} + +function parseValueCondition(value: unknown, location: string): ValueCondition { + const condition = requireObject(value, location); + switch (condition.type) { + case "comparison": { + const operator = parseComparisonOperator( + condition.operator, + `${location}.operator`, + ); + const requiresValue = operator !== "exists" && operator !== "does-not-exist"; + if (requiresValue && condition.value === undefined) { + throw new DeclareConstraintJsonError( + `${location}.value is required for operator "${operator}".`, + ); + } + if (!requiresValue && condition.value !== undefined) { + throw new DeclareConstraintJsonError( + `${location}.value must be omitted for operator "${operator}".`, + ); + } + return { + type: "comparison", + path: parseDataPath(condition.path, `${location}.path`), + operator, + ...(requiresValue + ? { value: parseJsonValue(condition.value, `${location}.value`) } + : {}), + }; + } + case "partial-object": + return { + type: "partial-object", + path: parseDataPath(condition.path, `${location}.path`), + value: parseJsonObjectValue(condition.value, `${location}.value`), + }; + case "contains-item": + return { + type: "contains-item", + path: parseDataPath(condition.path, `${location}.path`), + condition: parseValueCondition( + condition.condition, + `${location}.condition`, + ), + }; + case "group": + return { + type: "group", + operator: parseAndOr(condition.operator, `${location}.operator`), + conditions: requireArray(condition.conditions, `${location}.conditions`).map( + (child, index) => + parseValueCondition(child, `${location}.conditions[${index}]`), + ), + }; + default: + throw new DeclareConstraintJsonError( + `${location}.type must be "comparison", "partial-object", "contains-item", or "group".`, + ); + } +} + +function parseTransitionCondition( + value: unknown, + location: string, +): TransitionCondition { + const condition = requireObject(value, location); + switch (condition.type) { + case "source": + return { + type: "source", + source: parseDataSource(condition.source, `${location}.source`), + condition: parseValueCondition(condition.condition, `${location}.condition`), + }; + case "group": + return { + type: "group", + operator: parseAndOr(condition.operator, `${location}.operator`), + conditions: requireArray(condition.conditions, `${location}.conditions`).map( + (child, index) => + parseTransitionCondition(child, `${location}.conditions[${index}]`), + ), + }; + default: + throw new DeclareConstraintJsonError( + `${location}.type must be "source" or "group".`, + ); + } +} + +function parseCaptureDefinition( + value: unknown, + location: string, +): CaptureDefinition { + const capture = requireObject(value, location); + return { + alias: requireString(capture.alias, `${location}.alias`), + source: parseDataSource(capture.source, `${location}.source`), + path: parseDataPath(capture.path, `${location}.path`), + }; +} + +function parseCorrelationReference( + value: unknown, + location: string, +): CorrelationValueReference { + const reference = requireObject(value, location); + switch (reference.kind) { + case "literal": + return { + kind: "literal", + value: parseJsonValue(reference.value, `${location}.value`), + }; + case "activation": + return { + kind: "activation", + alias: requireString(reference.alias, `${location}.alias`), + }; + case "target": + return { + kind: "target", + source: parseDataSource(reference.source, `${location}.source`), + path: parseDataPath(reference.path, `${location}.path`), + }; + case "item": + return { + kind: "item", + path: parseDataPath(reference.path, `${location}.path`), + }; + default: + throw new DeclareConstraintJsonError( + `${location}.kind must be "literal", "activation", "target", or "item".`, + ); + } +} + +function parseCorrelationCondition( + value: unknown, + location: string, +): CorrelationCondition { + const condition = requireObject(value, location); + switch (condition.type) { + case "comparison": { + if ( + typeof condition.operator !== "string" || + !CORRELATION_COMPARISON_OPERATORS.has(condition.operator) + ) { + throw new DeclareConstraintJsonError( + `${location}.operator must be a supported correlation comparison operator.`, + ); + } + return { + type: "comparison", + left: parseCorrelationReference(condition.left, `${location}.left`), + operator: condition.operator as Extract< + CorrelationCondition, + { type: "comparison" } + >["operator"], + right: parseCorrelationReference(condition.right, `${location}.right`), + }; + } + case "reference-exists": + return { + type: "reference-exists", + reference: parseCorrelationReference( + condition.reference, + `${location}.reference`, + ), + exists: requireBoolean(condition.exists, `${location}.exists`), + }; + case "contains-item": + return { + type: "contains-item", + source: parseDataSource(condition.source, `${location}.source`), + path: parseDataPath(condition.path, `${location}.path`), + condition: parseCorrelationCondition( + condition.condition, + `${location}.condition`, + ), + }; + case "group": + return { + type: "group", + operator: parseAndOr(condition.operator, `${location}.operator`), + conditions: requireArray(condition.conditions, `${location}.conditions`).map( + (child, index) => + parseCorrelationCondition(child, `${location}.conditions[${index}]`), + ), + }; + default: + throw new DeclareConstraintJsonError( + `${location}.type must be "comparison", "reference-exists", "contains-item", or "group".`, + ); + } +} + +function parseTransitionMatcher( + value: unknown, + location: string, +): TransitionNameMatcher { + const matcher = requireObject(value, location); + if (matcher.operator !== "equals") { + throw new DeclareConstraintJsonError( + `${location}.operator must be "equals".`, + ); + } + return { + operator: "equals", + value: requireString(matcher.value, `${location}.value`), + }; +} + +function parsePredicate(value: unknown, location: string): DeclarePredicate { + const predicate = requireObject(value, location); + return { + ...(predicate.transition !== undefined + ? { + transition: parseTransitionMatcher( + predicate.transition, + `${location}.transition`, + ), + } + : {}), + ...(predicate.condition !== undefined + ? { + condition: parseTransitionCondition( + predicate.condition, + `${location}.condition`, + ), + } + : {}), + ...(predicate.captures !== undefined + ? { + captures: requireArray( + predicate.captures, + `${location}.captures`, + ).map((capture, index) => + parseCaptureDefinition(capture, `${location}.captures[${index}]`), + ), + } + : {}), + }; +} + +function parsePredicateGroup( + value: unknown, + location: string, +): DeclarePredicateGroup { + const group = requireObject(value, location); + return { + relation: parseAndOr(group.relation, `${location}.relation`) as ActivityRelation, + predicates: requireArray(group.predicates, `${location}.predicates`).map( + (predicate, index) => + parsePredicate(predicate, `${location}.predicates[${index}]`), + ), + }; +} + +function parseTemplateId(value: unknown, location: string): DeclareTemplateId { + const template = requireString(value, location); + if (!TEMPLATE_IDS.has(template)) { + throw new DeclareConstraintJsonError( + `${location} contains unknown Declare template "${template}".`, + ); + } + return template as DeclareTemplateId; +} + +function parseDeclareConstraint( + value: unknown, + location: string, +): DeclareConstraint { + const constraint = requireObject(value, location); + const count = constraint.count; + if ( + count !== undefined && + (typeof count !== "number" || !Number.isInteger(count) || count < 0) + ) { + throw new DeclareConstraintJsonError( + `${location}.count must be a non-negative integer when present.`, + ); + } + return { + id: requireNonEmptyString(constraint.id, `${location}.id`), + template: parseTemplateId(constraint.template, `${location}.template`), + enabled: requireBoolean(constraint.enabled, `${location}.enabled`), + ...(constraint.activation !== undefined + ? { + activation: parsePredicateGroup( + constraint.activation, + `${location}.activation`, + ), + } + : {}), + ...(constraint.target !== undefined + ? { + target: parsePredicateGroup(constraint.target, `${location}.target`), + } + : {}), + ...(constraint.between !== undefined + ? { + between: parsePredicateGroup( + constraint.between, + `${location}.between`, + ), + } + : {}), + ...(constraint.correlation !== undefined + ? { + correlation: parseCorrelationCondition( + constraint.correlation, + `${location}.correlation`, + ), + } + : {}), + ...(count !== undefined ? { count: count as number } : {}), + }; +} + +export function parseDeclareConstraintsJson( + value: unknown, + location = "declareConstraints", +): DeclareConstraint[] { + const constraints = requireArray(value, location).map((constraint, index) => + parseDeclareConstraint(constraint, `${location}[${index}]`), + ); + const ids = new Set(); + constraints.forEach((constraint) => { + if (ids.has(constraint.id)) { + throw new DeclareConstraintJsonError( + `Duplicate Declare constraint ID: ${constraint.id}.`, + ); + } + ids.add(constraint.id); + }); + return constraints; +} diff --git a/frontend/src/graph/graphJson.test.ts b/frontend/src/graph/graphJson.test.ts index 84c49b3..15d004f 100644 --- a/frontend/src/graph/graphJson.test.ts +++ b/frontend/src/graph/graphJson.test.ts @@ -441,3 +441,59 @@ describe("serialization and round trips", () => { expect(text.endsWith("\n")).toBe(true); }); }); + +describe("Declare constraint persistence", () => { + const constraints = [ + { + id: "persisted-response", + template: "response" as const, + enabled: true, + activation: { + relation: "or" as const, + predicates: [ + { + transition: { operator: "equals" as const, value: "A" }, + captures: [{ alias: "request_id", source: "inputs" as const, path: ["id"] }], + }, + ], + }, + target: { + relation: "or" as const, + predicates: [{ transition: { operator: "equals" as const, value: "B" } }], + }, + correlation: { + type: "comparison" as const, + left: { kind: "target" as const, source: "outputs" as const, path: ["id"] }, + operator: "=" as const, + right: { kind: "activation" as const, alias: "request_id" }, + }, + }, + ]; + + it("round-trips constraints with a full graph document", () => { + const document = createGraphJsonDocument(graph, undefined, constraints); + const reparsed = parseGraphJsonText(serializeGraphJson(document)); + expect(reparsed.declareConstraints).toEqual(constraints); + expect(reparsed.document.declareConstraints).toEqual(constraints); + }); + + it("round-trips constraints with a selected-path document", () => { + const path = { startNodeId: "0", edgeIds: ["e01a"] }; + const document = createSelectedPathJsonDocument( + graph, + path, + undefined, + constraints, + ); + + expect( + parseGraphJsonText(serializeGraphJson(document)).declareConstraints, + ).toEqual(constraints); + }); + + it("omits empty constraints and reads old documents as an empty list", () => { + const document = createGraphJsonDocument(graph); + expect(document).not.toHaveProperty("declareConstraints"); + expect(parseGraphJsonValue(document).declareConstraints).toEqual([]); + }); + }); diff --git a/frontend/src/graph/graphJson.ts b/frontend/src/graph/graphJson.ts index e406b9e..21cd1ba 100644 --- a/frontend/src/graph/graphJson.ts +++ b/frontend/src/graph/graphJson.ts @@ -1,3 +1,5 @@ +import type { DeclareConstraint } from "./declareConstraints"; +import { parseDeclareConstraintsJson } from "./declareConstraintJson"; import { resolvePath, type PathEdge, @@ -38,6 +40,7 @@ export interface GraphJsonDocument { metadata?: GraphJsonMetadata; nodes: JsonGraphNode[]; edges: JsonGraphEdge[]; + declareConstraints?: DeclareConstraint[]; } export interface SelectedPathJsonDocument { @@ -53,6 +56,7 @@ export interface SelectedPathJsonDocument { nodes: JsonGraphNode[]; edges: JsonGraphEdge[]; path: SelectedPath; + declareConstraints?: DeclareConstraint[]; } export type LtsVisualizerJsonDocument = @@ -63,6 +67,7 @@ export interface ParsedGraphJson { document: LtsVisualizerJsonDocument; graph: JsonGraphData; selectedPath: SelectedPath | null; + declareConstraints: DeclareConstraint[]; } export class GraphJsonError extends Error { @@ -261,6 +266,10 @@ function normalizeDocument(value: unknown): LtsVisualizerJsonDocument { ? "selected-path" : "graph"; const metadata = parseMetadata(root.metadata); + const declareConstraints = + root.declareConstraints === undefined + ? [] + : parseDeclareConstraintsJson(root.declareConstraints); if (type === "selected-path") { const selectedPath = parseSelectedPath(root.path); @@ -282,6 +291,7 @@ function normalizeDocument(value: unknown): LtsVisualizerJsonDocument { nodes, edges, path: selectedPath, + ...(declareConstraints.length > 0 ? { declareConstraints } : {}), }; } @@ -292,6 +302,7 @@ function normalizeDocument(value: unknown): LtsVisualizerJsonDocument { ...(metadata ? { metadata } : {}), nodes, edges, + ...(declareConstraints.length > 0 ? { declareConstraints } : {}), }; } @@ -314,12 +325,14 @@ export function parseGraphJsonValue(value: unknown): ParsedGraphJson { document, graph: { nodes: document.nodes, edges: document.edges }, selectedPath: document.type === "selected-path" ? document.path : null, + declareConstraints: document.declareConstraints ?? [], }; } export function createGraphJsonDocument( graph: JsonGraphData, - metadata?: GraphJsonMetadata + metadata?: GraphJsonMetadata, + declareConstraints: readonly DeclareConstraint[] = [], ): GraphJsonDocument { return parseGraphJsonValue({ format: "ltsvisualizer", @@ -332,13 +345,17 @@ export function createGraphJsonDocument( }, nodes: graph.nodes, edges: graph.edges, + ...(declareConstraints.length > 0 + ? { declareConstraints: structuredClone(declareConstraints) } + : {}), }).document as GraphJsonDocument; } export function createSelectedPathJsonDocument( graph: JsonGraphData, path: SelectedPath, - metadata?: GraphJsonMetadata + metadata?: GraphJsonMetadata, + declareConstraints: readonly DeclareConstraint[] = [], ): SelectedPathJsonDocument { const resolved = resolvePath(graph, path); const selectedNodeIds = new Set(resolved.nodeIds); @@ -362,6 +379,9 @@ export function createSelectedPathJsonDocument( nodes: pathGraph.nodes, edges: pathGraph.edges, path, + ...(declareConstraints.length > 0 + ? { declareConstraints: structuredClone(declareConstraints) } + : {}), }).document as SelectedPathJsonDocument; } From 2499da5c340702748597ec78c5630e579c8fb4df Mon Sep 17 00:00:00 2001 From: dbera Date: Sun, 9 Aug 2026 11:59:36 +0200 Subject: [PATCH 2/4] feat: persist path search configuration --- frontend/src/App.tsx | 35 +++++++-- frontend/src/graph/graphJson.test.ts | 105 +++++++++++++++++++++++++++ frontend/src/graph/graphJson.ts | 91 +++++++++++++++++++++++ 3 files changed, 225 insertions(+), 6 deletions(-) diff --git a/frontend/src/App.tsx b/frontend/src/App.tsx index 61ffecd..50d7b33 100644 --- a/frontend/src/App.tsx +++ b/frontend/src/App.tsx @@ -34,6 +34,7 @@ import { createSelectedPathJsonDocument, parseGraphJsonText, serializeGraphJson, + type PersistedPathSearchConfiguration, } from "./graph/graphJson"; import { useGraphAnalysis } from "./graph/useGraphAnalysis"; import { usePathSearch } from "./graph/usePathSearch"; @@ -660,6 +661,20 @@ function App() { URL.revokeObjectURL(url); } + function getPersistedPathSearchConfiguration(): PersistedPathSearchConfiguration { + const sourceNodeId = pathSearchSource.trim(); + const targetNodeId = pathSearchTarget.trim(); + return { + sourceNodeId, + endpointMode: targetNodeId + ? "specific-target" + : "constraint-satisfaction", + ...(targetNodeId ? { targetNodeId } : {}), + requestedPathCount, + maximumVisitsPerState, + requireConstraintExercise, + }; + } function exportFullGraphJson() { const graph = graphRef.current; if (!graph) { @@ -676,6 +691,7 @@ function App() { graph, { title: sourceName }, declareConstraints, + getPersistedPathSearchConfiguration(), ); const exportFileName = `${safeName}.json`; @@ -1135,9 +1151,16 @@ function App() { const defaultPathState = graph.nodes.some((node) => node.id === "0") ? "0" : graph.nodes[0].id; - setPathSearchSource(defaultPathState); - setPathSearchTarget(""); - setRequireConstraintExercise(true); + const importedPathSearch = parsed.pathSearch; + setPathSearchSource(importedPathSearch?.sourceNodeId ?? defaultPathState); + setPathSearchTarget(importedPathSearch?.targetNodeId ?? ""); + setRequestedPathCount(importedPathSearch?.requestedPathCount ?? 5); + setMaximumVisitsPerState( + importedPathSearch?.maximumVisitsPerState ?? 1, + ); + setRequireConstraintExercise( + importedPathSearch?.requireConstraintExercise ?? true, + ); if (importedPath) { const resolved = resolvePath(graph, importedPath); @@ -2179,7 +2202,7 @@ function App() { > Cyclic component {getCyclicComponentNumber(component.id)} - {component.nodeIds.length} states ·{" "} + {component.nodeIds.length} states{" \u00b7 "} {component.internalEdgeIds.length} transitions @@ -2394,7 +2417,7 @@ function App() { {path.edgeIds.length} transition {path.edgeIds.length === 1 ? "" : "s"} - {` · Ends at state ${ + {` \u00b7 Ends at state ${ path.endNodeId ?? steps.at(-1)?.target ?? path.startNodeId @@ -2440,7 +2463,7 @@ function App() { > {step.source} - + + {(path.explanations?.length ?? 0) > 0 && ( +
+ Why this path satisfies the constraints +
+ {path.explanations?.map((explanation) => ( +
+
+ {explanation.constraintId} + Satisfied +
+ {explanation.template} +

{explanation.summary}

+

+ {explanation.exercised + ? "Constraint was exercised by this path." + : "Constraint was satisfied without an exercise event."} +

+ {explanation.events.length > 0 && ( +
    + {explanation.events.map((explanationEvent, eventIndex) => ( +
  1. + +
    2. + ))} +
+ )} +
+ ))} +
+
+ )}
Show transition details {steps.length === 0 ? ( diff --git a/frontend/src/graph/pathSearch.test.ts b/frontend/src/graph/pathSearch.test.ts index ff95071..33d5537 100644 --- a/frontend/src/graph/pathSearch.test.ts +++ b/frontend/src/graph/pathSearch.test.ts @@ -592,13 +592,12 @@ describe("findKShortestBoundedPaths", () => { constraints: { declare: [responseConstraint] }, }); - expect(result.paths).toEqual([ - { - startNodeId: "source", - endNodeId: "satisfied", - edgeIds: ["a", "b"], - }, - ]); + expect(result.paths).toHaveLength(1); + expect(result.paths[0]).toMatchObject({ + startNodeId: "source", + endNodeId: "satisfied", + edgeIds: ["a", "b"], + }); }); it("rejects vacuous Response satisfaction when exercise is required", () => { @@ -632,9 +631,12 @@ describe("findKShortestBoundedPaths", () => { constraints: { declare: [responseConstraint] }, }); - expect(result.paths).toEqual([ - { startNodeId: "source", endNodeId: "source", edgeIds: [] }, - ]); + expect(result.paths).toHaveLength(1); + expect(result.paths[0]).toMatchObject({ + startNodeId: "source", + endNodeId: "source", + edgeIds: [], + }); }); it("does not treat only a Precedence activation as exercise", () => { @@ -678,9 +680,12 @@ describe("findKShortestBoundedPaths", () => { }, }); - expect(result.paths).toEqual([ - { startNodeId: "source", endNodeId: "source", edgeIds: [] }, - ]); + expect(result.paths).toHaveLength(1); + expect(result.paths[0]).toMatchObject({ + startNodeId: "source", + endNodeId: "source", + edgeIds: [], + }); }); it("requires at least one enabled constraint without a target", () => { @@ -715,4 +720,120 @@ describe("findKShortestBoundedPaths", () => { }); }); + it("explains data-aware Response and cardinality satisfaction", () => { + const result = findKShortestBoundedPaths({ + nodeIds: ["0", "1", "2", "3"], + edges: [ + { id: "audit", source: "0", target: "1", transition: "Audit", inputs: { events: [[{ type: "login" }]] } }, + { id: "login", source: "1", target: "2", transition: "Login", inputs: { credentials: [{ userName: "xyz" }] } }, + { id: "complete", source: "2", target: "3", transition: "Complete" }, + ], + sourceNodeId: "0", + targetNodeId: "3", + requestedPathCount: 1, + maximumVisitsPerState: 1, + constraints: { declare: [ + { + id: "login-response", + template: "response", + enabled: true, + activation: { relation: "or", predicates: [{ transition: { operator: "equals", value: "Login" }, condition: { type: "source", source: "inputs", condition: { type: "contains-item", path: ["credentials"], condition: { type: "comparison", path: ["userName"], operator: "=", value: "xyz" } } } }] }, + target: { relation: "or", predicates: [{ transition: { operator: "equals", value: "Complete" } }] }, + }, + { + id: "audit-count", + template: "at-least", + enabled: true, + count: 1, + activation: { relation: "or", predicates: [{ transition: { operator: "equals", value: "Audit" }, condition: { type: "source", source: "inputs", condition: { type: "contains-item", path: ["events"], condition: { type: "comparison", path: [0, "type"], operator: "=", value: "login" } } } }] }, + }, + ] }, + }); + expect(result.paths[0].explanations).toEqual([ + { + constraintId: "login-response", template: "response", status: "satisfied", exercised: true, + summary: "1 activation fulfilled.", + events: [ + { role: "activation", stepNumber: 2, edgeId: "login", transition: "Login" }, + { role: "fulfillment", stepNumber: 3, edgeId: "complete", transition: "Complete" }, + ], + }, + { + constraintId: "audit-count", template: "at-least", status: "satisfied", exercised: true, + summary: "Matched 1 time; required count 1.", + events: [{ role: "match", stepNumber: 1, edgeId: "audit", transition: "Audit" }], + }, + ]); + }); + + + it("explains position, choice, and precedence template families", () => { + const result = findKShortestBoundedPaths({ + nodeIds: ["0", "1", "2", "3"], + edges: [ + { id: "a", source: "0", target: "1", transition: "A" }, + { id: "x", source: "1", target: "2", transition: "X" }, + { id: "b", source: "2", target: "3", transition: "B" }, + ], + sourceNodeId: "0", + targetNodeId: "3", + requestedPathCount: 1, + maximumVisitsPerState: 1, + constraints: { declare: [ + { id: "init-a", template: "init", enabled: true, activation: { relation: "or", predicates: [{ transition: { operator: "equals", value: "A" } }] } }, + { id: "choice-a-c", template: "choice", enabled: true, activation: { relation: "or", predicates: [{ transition: { operator: "equals", value: "A" } }] }, target: { relation: "or", predicates: [{ transition: { operator: "equals", value: "C" } }] } }, + { id: "a-before-b", template: "precedence", enabled: true, activation: { relation: "or", predicates: [{ transition: { operator: "equals", value: "A" } }] }, target: { relation: "or", predicates: [{ transition: { operator: "equals", value: "B" } }] } }, + ] }, + }); + expect(result.paths[0].explanations).toEqual(expect.arrayContaining([ + expect.objectContaining({ + constraintId: "init-a", + summary: "The first transition matches the Init activation.", + events: [expect.objectContaining({ role: "position-match", edgeId: "a", stepNumber: 1 })], + }), + expect.objectContaining({ + constraintId: "choice-a-c", + summary: "Activation side occurred, satisfying Choice.", + events: [expect.objectContaining({ role: "choice-match", edgeId: "a" })], + }), + expect.objectContaining({ + constraintId: "a-before-b", + summary: "Every target had a qualifying preceding activation.", + events: [ + expect.objectContaining({ role: "preceding-support", edgeId: "a" }), + expect.objectContaining({ role: "target", edgeId: "b" }), + ], + }), + ])); + }); + + it("explains negative templates as avoided forbidden relationships", () => { + const result = findKShortestBoundedPaths({ + nodeIds: ["0", "1", "2", "3"], + edges: [ + { id: "a", source: "0", target: "1", transition: "A", inputs: { id: 10 } }, + { id: "b-wrong", source: "1", target: "2", transition: "B", outputs: { id: 20 } }, + { id: "x", source: "2", target: "3", transition: "X" }, + ], + sourceNodeId: "0", + targetNodeId: "3", + requestedPathCount: 1, + maximumVisitsPerState: 1, + constraints: { declare: [{ + id: "not-correlated-response", + template: "not-response", + enabled: true, + activation: { relation: "or", predicates: [{ transition: { operator: "equals", value: "A" }, captures: [{ alias: "id", source: "inputs", path: ["id"] }] }] }, + target: { relation: "or", predicates: [{ transition: { operator: "equals", value: "B" } }] }, + correlation: { type: "comparison", left: { kind: "target", source: "outputs", path: ["id"] }, operator: "=", right: { kind: "activation", alias: "id" } }, + }] }, + }); + expect(result.paths[0].explanations?.[0]).toMatchObject({ + constraintId: "not-correlated-response", + status: "satisfied", + exercised: true, + summary: "No forbidden correlated activation-target relationship occurred.", + }); + }); + }); diff --git a/frontend/src/graph/pathSearch.ts b/frontend/src/graph/pathSearch.ts index 9c8302e..04285b0 100644 --- a/frontend/src/graph/pathSearch.ts +++ b/frontend/src/graph/pathSearch.ts @@ -1,4 +1,6 @@ -import type { DeclareConstraint } from "./declareConstraints"; +import type { DeclareConstraint, DeclareTemplateId } from "./declareConstraints"; +import { evaluateDeclarePredicateGroup } from "./declarePredicates"; +import { evaluateCorrelationCondition, type ActivationBindings } from "./transitionCorrelation"; import { advanceMonitorSet, createMonitorSet, @@ -39,10 +41,34 @@ export type PathSearchInput = { constraints?: PathConstraints; }; +export type ConstraintExplanationEvent = { + role: + | "activation" + | "target" + | "fulfillment" + | "match" + | "preceding-support" + | "immediate-support" + | "position-match" + | "choice-match" + | "forbidden-pair-avoided"; + stepNumber: number; + edgeId: string; + transition: string; +}; +export type ConstraintExplanation = { + constraintId: string; + template: DeclareTemplateId; + status: "satisfied"; + exercised: boolean; + summary: string; + events: ConstraintExplanationEvent[]; +}; export type BoundedPath = { startNodeId: string; endNodeId?: string; edgeIds: string[]; + explanations?: ConstraintExplanation[]; }; export type PathSearchStopReason = @@ -343,6 +369,215 @@ function reconstructEdgeIds(candidate: SearchCandidate): string[] { function createPathKey(edgeIds: string[]): string { return JSON.stringify(edgeIds); } +type IndexedPredicateMatch = { + stepNumber: number; + edge: PathSearchEdge; + bindings: ActivationBindings; +}; +function predicateMatches( + group: DeclareConstraint["activation"], + edges: readonly PathSearchEdge[], +): IndexedPredicateMatch[] { + if (!group) return []; + return edges.flatMap((edge, index) => { + const evaluation = evaluateDeclarePredicateGroup(group, edge); + return evaluation.matches + ? evaluation.predicateMatches.map((match) => ({ + stepNumber: index + 1, + edge, + bindings: match.bindings, + })) + : []; + }); +} +function event( + role: ConstraintExplanationEvent["role"], + match: IndexedPredicateMatch, +): ConstraintExplanationEvent { + return { + role, + stepNumber: match.stepNumber, + edgeId: match.edge.id, + transition: match.edge.transition ?? match.edge.id, + }; +} +function matchesCorrelation( + constraint: DeclareConstraint, + activation: IndexedPredicateMatch, + target: IndexedPredicateMatch, +): boolean { + return !constraint.correlation || evaluateCorrelationCondition( + constraint.correlation, + target.edge, + activation.bindings, + ).matches; +} +function betweenMatches( + constraint: DeclareConstraint, + edges: readonly PathSearchEdge[], + startStep: number, + endStep: number, +): boolean { + if (!constraint.between) return false; + return edges.slice(startStep, endStep - 1).some((edge) => + evaluateDeclarePredicateGroup(constraint.between!, edge).matches, + ); +} +function explainConstraint( + constraint: DeclareConstraint, + edges: readonly PathSearchEdge[], + compiled: CompiledDeclareConstraint, +): ConstraintExplanation { + const activations = predicateMatches(constraint.activation, edges); + const targets = predicateMatches(constraint.target, edges); + const exercised = edges.some((edge) => compiled.isExercisedBy(edge)); + const events: ConstraintExplanationEvent[] = []; + let summary: string; + switch (constraint.template) { + case "at-least": + case "at-most": + case "exactly": + case "exactly-consecutive": + events.push(...activations.map((match) => event("match", match))); + summary = constraint.template === "exactly-consecutive" + ? `Matched one consecutive run of ${activations.length}; required count ${constraint.count ?? 0}.` + : `Matched ${activations.length} time${activations.length === 1 ? "" : "s"}; required count ${constraint.count ?? 0}.`; + break; + case "init": + if (activations[0]) events.push(event("position-match", activations[0])); + summary = "The first transition matches the Init activation."; + break; + case "end": { + const last = activations.find((match) => match.stepNumber === edges.length); + if (last) events.push(event("position-match", last)); + summary = "The final transition matches the End activation."; + break; + } + case "choice": + case "exclusive-choice": + events.push(...activations.map((match) => event("choice-match", match))); + events.push(...targets.map((match) => event("choice-match", match))); + summary = constraint.template === "choice" + ? `${activations.length > 0 ? "Activation" : "Target"} side occurred, satisfying Choice.` + : `Exactly one side occurred: ${activations.length > 0 ? "activation" : "target"}.`; + break; + case "response": + case "chain-response": + case "alternate-response": + case "responded-existence": + case "succession": + case "chain-succession": + case "alternate-succession": { + for (const activation of activations) { + events.push(event("activation", activation)); + const fulfillment = targets.find((target) => { + const orderOkay = constraint.template === "responded-existence" + ? true + : target.stepNumber > activation.stepNumber; + const chainOkay = !["chain-response", "chain-succession"].includes(constraint.template) || + target.stepNumber === activation.stepNumber + 1; + const alternateOkay = !["alternate-response", "alternate-succession"].includes(constraint.template) || + !betweenMatches(constraint, edges, activation.stepNumber, target.stepNumber); + return orderOkay && chainOkay && alternateOkay && + matchesCorrelation(constraint, activation, target); + }); + if (fulfillment) events.push(event("fulfillment", fulfillment)); + } + if (constraint.template.includes("succession")) { + summary = activations.length === 0 && targets.length === 0 + ? "Satisfied vacuously: neither side occurred." + : `${activations.length} activation${activations.length === 1 ? "" : "s"} fulfilled, and every target had the required preceding activation.`; + } else { + summary = activations.length === 0 + ? "Satisfied vacuously: no matching activation occurred." + : `${activations.length} activation${activations.length === 1 ? "" : "s"} fulfilled.`; + } + break; + } + case "precedence": + case "chain-precedence": + case "alternate-precedence": { + for (const target of targets) { + const support = [...activations].reverse().find((activation) => { + const orderOkay = activation.stepNumber < target.stepNumber; + const chainOkay = constraint.template !== "chain-precedence" || + activation.stepNumber === target.stepNumber - 1; + const alternateOkay = constraint.template !== "alternate-precedence" || + !betweenMatches(constraint, edges, activation.stepNumber, target.stepNumber); + return orderOkay && chainOkay && alternateOkay && + matchesCorrelation(constraint, activation, target); + }); + if (support) { + events.push(event( + constraint.template === "chain-precedence" + ? "immediate-support" + : "preceding-support", + support, + )); + } + events.push(event("target", target)); + } + summary = targets.length === 0 + ? "Satisfied vacuously: no matching target occurred." + : `Every target had ${constraint.template === "chain-precedence" ? "an immediate" : "a qualifying"} preceding activation.`; + break; + } + case "coexistence": { + events.push(...activations.map((match) => event("activation", match))); + events.push(...targets.map((match) => event("target", match))); + summary = activations.length === 0 && targets.length === 0 + ? "Satisfied vacuously: neither side occurred." + : "Activation and target both occurred with correlated counterparts."; + break; + } + case "not-response": + case "not-chain-response": + case "not-alternate-response": + case "not-precedence": + case "not-chain-precedence": + case "not-alternate-precedence": + case "not-responded-existence": + case "not-coexistence": + case "not-succession": + case "not-chain-succession": + case "not-alternate-succession": + events.push(...activations.map((match) => event("activation", match))); + events.push(...targets.map((match) => event("target", match))); + if (events[0]) events[0] = { ...events[0], role: "forbidden-pair-avoided" }; + summary = activations.length === 0 && targets.length === 0 + ? "Satisfied vacuously: neither constrained event occurred." + : "No forbidden correlated activation-target relationship occurred."; + break; + } + return { + constraintId: constraint.id, + template: constraint.template, + status: "satisfied", + exercised, + summary, + events, + }; +} +function explainAcceptedPath( + edgeIds: readonly string[], + edgesById: ReadonlyMap, + constraints: readonly DeclareConstraint[], + compiledConstraints: readonly CompiledDeclareConstraint[], +): ConstraintExplanation[] { + const edges = edgeIds.map((edgeId) => { + const edge = edgesById.get(edgeId); + if (!edge) throw new Error(`Cannot explain unknown edge ${edgeId}.`); + return edge; + }); + const compiledById = new Map(compiledConstraints.map((item) => [item.id, item])); + return constraints + .filter((constraint) => constraint.enabled) + .map((constraint) => { + const compiled = compiledById.get(constraint.id); + if (!compiled) throw new Error(`Cannot explain uncompiled constraint ${constraint.id}.`); + return explainConstraint(constraint, edges, compiled); + }); +} function resolveEndpointMode(input: PathSearchInput): PathSearchEndpointMode { return input.endpointMode ?? @@ -410,9 +645,9 @@ export function findKShortestBoundedPaths( "Maximum queued candidates", ); - const compiledConstraints = compileDeclareConstraints( - input.constraints?.declare ?? [], - ); + const declareConstraints = input.constraints?.declare ?? []; + const compiledConstraints = compileDeclareConstraints(declareConstraints); + const edgesById = new Map(input.edges.map((edge) => [edge.id, edge])); const initialMonitorEntries = createMonitorSet(compiledConstraints); const requireConstraintExercise = endpointMode === "constraint-satisfaction" && @@ -497,6 +732,16 @@ export function findKShortestBoundedPaths( ? { endNodeId: candidate.currentNodeId } : {}), edgeIds, + ...(compiledConstraints.length > 0 + ? { + explanations: explainAcceptedPath( + edgeIds, + edgesById, + declareConstraints, + compiledConstraints, + ), + } + : {}), }); } From 2540d5bb771a34433a3878eb3fe0235f6ddd3477 Mon Sep 17 00:00:00 2001 From: dbera Date: Tue, 11 Aug 2026 00:59:28 +0200 Subject: [PATCH 4/4] fix: align alternative templates to be declare compliant and enforce constraint exercise for targeted paths --- frontend/src/App.tsx | 5 +- .../src/graph/DeclareConstraintBuilder.tsx | 25 ---- frontend/src/graph/declareConstraintJson.ts | 8 -- frontend/src/graph/declareConstraints.test.ts | 4 +- frontend/src/graph/declareConstraints.ts | 19 +-- .../src/graph/declareMonitorFactory.test.ts | 3 - frontend/src/graph/declareMonitorFactory.ts | 54 +------- .../graph/declarePrecedenceMonitors.test.ts | 55 +------- .../src/graph/declarePrecedenceMonitors.ts | 109 +++------------- .../src/graph/declareResponseMonitors.test.ts | 66 ++++------ frontend/src/graph/declareResponseMonitors.ts | 119 ++--------------- .../graph/declareSuccessionMonitors.test.ts | 33 +---- .../src/graph/declareSuccessionMonitors.ts | 39 +----- frontend/src/graph/pathSearch.test.ts | 121 ++++++++++++++++++ frontend/src/graph/pathSearch.ts | 26 +--- 15 files changed, 204 insertions(+), 482 deletions(-) diff --git a/frontend/src/App.tsx b/frontend/src/App.tsx index f0eeaf8..dd7a947 100644 --- a/frontend/src/App.tsx +++ b/frontend/src/App.tsx @@ -2365,8 +2365,9 @@ function App() {

Without a target, paths may end at any state after all enabled - constraints are satisfied. Exercise checking prevents vacuous - matches where a constraint never participates. + constraints are satisfied. When exercise checking is enabled, + returned paths must exercise every enabled constraint that + requires exercise.

diff --git a/frontend/src/graph/DeclareConstraintBuilder.tsx b/frontend/src/graph/DeclareConstraintBuilder.tsx index a5520da..4c1af90 100644 --- a/frontend/src/graph/DeclareConstraintBuilder.tsx +++ b/frontend/src/graph/DeclareConstraintBuilder.tsx @@ -87,9 +87,6 @@ export default function DeclareConstraintBuilder({ target: definition.requiredRoles.includes("target") ? constraint.target ?? group() : undefined, - between: definition.requiredRoles.includes("between") - ? constraint.between ?? group() - : undefined, count: definition.supportsCount ? constraint.count ?? 1 : undefined, }; }); @@ -263,28 +260,6 @@ export default function DeclareConstraintBuilder({ /> )} - {definition.requiredRoles.includes("between") && ( - <> - - changeTransition(constraint.id, "between", value) - } - /> - - changeCondition(constraint.id, "between", condition) - } - /> - - )} {definition.supportsCount && (