diff --git a/frontend/src/App.css b/frontend/src/App.css
index b2deee5..310aa3f 100644
--- a/frontend/src/App.css
+++ b/frontend/src/App.css
@@ -1223,3 +1223,18 @@ body.resizing-side-panel canvas {
line-height: 1.35;
}
+
+.computed-path-explanations { border-top: 1px solid #e2e8f0; }
+.computed-path-explanations > summary { padding: 8px 10px; color: #1d4ed8; font-size: 11px; font-weight: 750; cursor: pointer; }
+.constraint-explanation-list { display: grid; gap: 8px; padding: 8px 10px 10px; background: #f8fafc; }
+.constraint-explanation { padding: 9px; border: 1px solid #bbf7d0; border-radius: 7px; background: #f0fdf4; }
+.constraint-explanation-heading { display: flex; align-items: center; justify-content: space-between; gap: 8px; }
+.constraint-explanation-heading strong { color: #14532d; font-size: 11px; overflow-wrap: anywhere; }
+.constraint-explanation-heading span { padding: 2px 6px; border-radius: 999px; background: #dcfce7; color: #166534; font-size: 9px; font-weight: 800; }
+.constraint-explanation > small { display: block; margin-top: 2px; color: #64748b; font-size: 9px; }
+.constraint-explanation > p { margin: 6px 0 0; color: #334155; font-size: 10px; line-height: 1.4; }
+.constraint-explanation .constraint-exercise-status { color: #64748b; }
+.constraint-explanation ol { display: grid; gap: 4px; margin: 7px 0 0; padding-left: 20px; }
+.constraint-explanation li { color: #475569; font-size: 10px; }
+.constraint-explanation li button { padding: 0; border: 0; background: transparent; color: #2563eb; font-size: 10px; text-align: left; overflow-wrap: anywhere; }
+.constraint-explanation li button:hover { color: #1d4ed8; text-decoration: underline; }
diff --git a/frontend/src/App.tsx b/frontend/src/App.tsx
index 1ed0c42..dd7a947 100644
--- a/frontend/src/App.tsx
+++ b/frontend/src/App.tsx
@@ -34,10 +34,11 @@ import {
createSelectedPathJsonDocument,
parseGraphJsonText,
serializeGraphJson,
+ type PersistedPathSearchConfiguration,
} from "./graph/graphJson";
import { useGraphAnalysis } from "./graph/useGraphAnalysis";
import { usePathSearch } from "./graph/usePathSearch";
-import type { BoundedPath } from "./graph/pathSearch";
+import type { BoundedPath, ConstraintExplanationEvent } from "./graph/pathSearch";
import type { StronglyConnectedComponent } from "./graph/graphAnalysis";
import { buildTransitionCatalogue } from "./graph/transitionCatalog";
import { buildTransitionDataCatalogue } from "./graph/transitionDataCatalogue";
@@ -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) {
@@ -672,9 +687,12 @@ 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,
+ getPersistedPathSearchConfiguration(),
+ );
const exportFileName = `${safeName}.json`;
downloadTextFile(
@@ -722,9 +740,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 +1136,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);
@@ -1127,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);
@@ -1685,6 +1716,15 @@ function App() {
setStatus(`Focused state ${nodeId}`);
}
+ function focusExplanationEvent(
+ explanationEvent: ConstraintExplanationEvent,
+ pathIndex: number,
+ ) {
+ focusComputedPathEdge(
+ explanationEvent.edgeId,
+ `explanation-${pathIndex}-${explanationEvent.stepNumber}-${explanationEvent.edgeId}`,
+ );
+ }
function getComputedPathSteps(path: BoundedPath) {
const graph = graphRef.current;
if (!graph) return [];
@@ -2171,7 +2211,7 @@ function App() {
>
Cyclic component {getCyclicComponentNumber(component.id)}
- {component.nodeIds.length} states ·{" "}
+ {component.nodeIds.length} states{" \u00b7 "}
{component.internalEdgeIds.length} transitions
@@ -2325,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.
@@ -2386,13 +2427,53 @@ 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
}`}
+ {(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) => (
+
+ focusExplanationEvent(explanationEvent, index)}
+ >
+ {explanationEvent.role}: step {explanationEvent.stepNumber}{" "}
+ {explanationEvent.transition} ({explanationEvent.edgeId})
+
+
+ ))}
+
+ )}
+
+ ))}
+
+ )}
Show transition details
{steps.length === 0 ? (
@@ -2432,7 +2513,7 @@ function App() {
>
{step.source}
- →
+ {"\u2192"}
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 && (
Count N
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..8e80940
--- /dev/null
+++ b/frontend/src/graph/declareConstraintJson.ts
@@ -0,0 +1,501 @@
+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.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/declareConstraints.test.ts b/frontend/src/graph/declareConstraints.test.ts
index e914107..dfdce1a 100644
--- a/frontend/src/graph/declareConstraints.test.ts
+++ b/frontend/src/graph/declareConstraints.test.ts
@@ -19,7 +19,7 @@ const predicate = (name: string): DeclarePredicateGroup => ({
describe("Declare template registry", () => {
it("contains the complete planned template catalog with unique IDs", () => {
- expect(DECLARE_TEMPLATE_DEFINITIONS).toHaveLength(30);
+ expect(DECLARE_TEMPLATE_DEFINITIONS).toHaveLength(27);
const ids = DECLARE_TEMPLATE_DEFINITIONS.map((definition) => definition.id);
expect(new Set(ids).size).toBe(ids.length);
});
@@ -39,7 +39,7 @@ describe("Declare template registry", () => {
});
expect(getDeclareTemplateDefinition("alternate-succession")).toMatchObject({
category: "bidirectional",
- requiredRoles: ["activation", "target", "between"],
+ requiredRoles: ["activation", "target"],
});
});
});
diff --git a/frontend/src/graph/declareConstraints.ts b/frontend/src/graph/declareConstraints.ts
index cf4ca8e..ff60451 100644
--- a/frontend/src/graph/declareConstraints.ts
+++ b/frontend/src/graph/declareConstraints.ts
@@ -22,19 +22,16 @@ export type DeclareTemplateId =
| "chain-response"
| "not-chain-response"
| "alternate-response"
- | "not-alternate-response"
| "precedence"
| "not-precedence"
| "chain-precedence"
| "not-chain-precedence"
| "alternate-precedence"
- | "not-alternate-precedence"
| "succession"
| "not-succession"
| "chain-succession"
| "not-chain-succession"
- | "alternate-succession"
- | "not-alternate-succession";
+ | "alternate-succession";
export type DeclareTemplateCategory =
| "cardinality"
@@ -45,7 +42,7 @@ export type DeclareTemplateCategory =
| "past"
| "bidirectional";
-export type DeclarePredicateRole = "activation" | "target" | "between";
+export type DeclarePredicateRole = "activation" | "target";
export type ActivityRelation = "and" | "or";
export type TransitionNameMatcher = {
@@ -70,7 +67,6 @@ export type DeclareConstraint = {
enabled: boolean;
activation?: DeclarePredicateGroup;
target?: DeclarePredicateGroup;
- between?: DeclarePredicateGroup;
correlation?: CorrelationCondition;
count?: number;
};
@@ -102,20 +98,17 @@ const DEFINITIONS: readonly DeclareTemplateDefinition[] = [
{ id: "not-response", displayName: "Not response", category: "future", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "No activation is followed later by a correlated target." },
{ id: "chain-response", displayName: "Chain response", category: "future", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Every activation is immediately followed by a correlated target." },
{ id: "not-chain-response", displayName: "Not chain response", category: "future", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "No activation is immediately followed by a correlated target." },
- { id: "alternate-response", displayName: "Alternate response", category: "future", requiredRoles: ["activation", "target", "between"], supportsCount: false, supportsCorrelation: true, description: "Every activation is followed by a correlated target without another qualifying activation or forbidden between event." },
- { id: "not-alternate-response", displayName: "Not alternate response", category: "future", requiredRoles: ["activation", "target", "between"], supportsCount: false, supportsCorrelation: true, description: "Specialized negative alternate-response semantics." },
+ { id: "alternate-response", displayName: "Alternate response", category: "future", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Every activation is followed by a correlated target before another qualifying activation occurs." },
{ id: "precedence", displayName: "Precedence", category: "past", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Every target has a correlated activation before it." },
{ id: "not-precedence", displayName: "Not precedence", category: "past", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "No target has a correlated activation before it." },
{ id: "chain-precedence", displayName: "Chain precedence", category: "past", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Every target is immediately preceded by a correlated activation." },
{ id: "not-chain-precedence", displayName: "Not chain precedence", category: "past", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "No target is immediately preceded by a correlated activation." },
- { id: "alternate-precedence", displayName: "Alternate precedence", category: "past", requiredRoles: ["activation", "target", "between"], supportsCount: false, supportsCorrelation: true, description: "Every target has a correlated activation before it without another qualifying target or forbidden between event." },
- { id: "not-alternate-precedence", displayName: "Not alternate precedence", category: "past", requiredRoles: ["activation", "target", "between"], supportsCount: false, supportsCorrelation: true, description: "Specialized negative alternate-precedence semantics." },
+ { id: "alternate-precedence", displayName: "Alternate precedence", category: "past", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Every target has a correlated activation before it and after the previous qualifying target." },
{ id: "succession", displayName: "Succession", category: "bidirectional", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Response and precedence both hold." },
{ id: "not-succession", displayName: "Not succession", category: "bidirectional", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Negative succession semantics." },
{ id: "chain-succession", displayName: "Chain succession", category: "bidirectional", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Chain response and chain precedence both hold." },
{ id: "not-chain-succession", displayName: "Not chain succession", category: "bidirectional", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Negative chain-succession semantics." },
- { id: "alternate-succession", displayName: "Alternate succession", category: "bidirectional", requiredRoles: ["activation", "target", "between"], supportsCount: false, supportsCorrelation: true, description: "Alternate response and alternate precedence both hold." },
- { id: "not-alternate-succession", displayName: "Not alternate succession", category: "bidirectional", requiredRoles: ["activation", "target", "between"], supportsCount: false, supportsCorrelation: true, description: "Specialized negative alternate-succession semantics." },
+ { id: "alternate-succession", displayName: "Alternate succession", category: "bidirectional", requiredRoles: ["activation", "target"], supportsCount: false, supportsCorrelation: true, description: "Alternate response and alternate precedence both hold." },
] as const;
export const DECLARE_TEMPLATE_DEFINITIONS: readonly DeclareTemplateDefinition[] =
@@ -187,7 +180,7 @@ export function validateDeclareConstraint(
errors.push(`${definition.displayName} does not support correlation conditions.`);
}
- for (const role of ["activation", "target", "between"] as const) {
+ for (const role of ["activation", "target"] as const) {
if (!definition.requiredRoles.includes(role) && constraint[role]) {
errors.push(`${definition.displayName} does not use ${role}.`);
}
diff --git a/frontend/src/graph/declareMonitorFactory.test.ts b/frontend/src/graph/declareMonitorFactory.test.ts
index 6008a94..327990c 100644
--- a/frontend/src/graph/declareMonitorFactory.test.ts
+++ b/frontend/src/graph/declareMonitorFactory.test.ts
@@ -35,9 +35,6 @@ function constraintFor(template: DeclareTemplateId): DeclareConstraint {
target: definition.requiredRoles.includes("target")
? group("B")
: undefined,
- between: definition.requiredRoles.includes("between")
- ? group("C")
- : undefined,
count: definition.supportsCount ? 1 : undefined,
};
}
diff --git a/frontend/src/graph/declareMonitorFactory.ts b/frontend/src/graph/declareMonitorFactory.ts
index f218b75..4ac8ac1 100644
--- a/frontend/src/graph/declareMonitorFactory.ts
+++ b/frontend/src/graph/declareMonitorFactory.ts
@@ -27,7 +27,6 @@ import {
import {
createAlternatePrecedenceMonitor,
createChainPrecedenceMonitor,
- createNotAlternatePrecedenceMonitor,
createNotChainPrecedenceMonitor,
createNotPrecedenceMonitor,
createPrecedenceMonitor,
@@ -35,7 +34,6 @@ import {
import {
createAlternateResponseMonitor,
createChainResponseMonitor,
- createNotAlternateResponseMonitor,
createNotChainResponseMonitor,
createNotResponseMonitor,
createResponseMonitor,
@@ -43,7 +41,6 @@ import {
import {
createAlternateSuccessionMonitor,
createChainSuccessionMonitor,
- createNotAlternateSuccessionMonitor,
createNotChainSuccessionMonitor,
createNotSuccessionMonitor,
createSuccessionMonitor,
@@ -62,7 +59,7 @@ export type CompiledDeclareConstraint = {
function requireGroup(
constraint: DeclareConstraint,
- role: "activation" | "target" | "between",
+ role: "activation" | "target",
): DeclarePredicateGroup {
const group = constraint[role];
if (!group) {
@@ -115,7 +112,6 @@ export function createDeclareMonitor(
const activation = requireGroup(constraint, "activation");
const target = () => requireGroup(constraint, "target");
- const between = () => requireGroup(constraint, "between");
const count = () => constraint.count ?? 0;
const correlation = constraint.correlation;
@@ -165,19 +161,8 @@ export function createDeclareMonitor(
correlation,
);
case "alternate-response":
- return createAlternateResponseMonitor(
- activation,
- target(),
- between(),
- correlation,
- );
- case "not-alternate-response":
- return createNotAlternateResponseMonitor(
- activation,
- target(),
- between(),
- correlation,
- );
+ return createAlternateResponseMonitor(activation, target(), correlation);
+
case "precedence":
return createPrecedenceMonitor(activation, target(), correlation);
case "not-precedence":
@@ -191,19 +176,8 @@ export function createDeclareMonitor(
correlation,
);
case "alternate-precedence":
- return createAlternatePrecedenceMonitor(
- activation,
- target(),
- between(),
- correlation,
- );
- case "not-alternate-precedence":
- return createNotAlternatePrecedenceMonitor(
- activation,
- target(),
- between(),
- correlation,
- );
+ return createAlternatePrecedenceMonitor(activation, target(), correlation);
+
case "succession":
return createSuccessionMonitor(activation, target(), correlation);
case "not-succession":
@@ -217,19 +191,8 @@ export function createDeclareMonitor(
correlation,
);
case "alternate-succession":
- return createAlternateSuccessionMonitor(
- activation,
- target(),
- between(),
- correlation,
- );
- case "not-alternate-succession":
- return createNotAlternateSuccessionMonitor(
- activation,
- target(),
- between(),
- correlation,
- );
+ return createAlternateSuccessionMonitor(activation, target(), correlation);
+
}
}
@@ -270,14 +233,12 @@ function createExercisePolicy(constraint: DeclareConstraint): Pick<
case "chain-precedence":
case "not-chain-precedence":
case "alternate-precedence":
- case "not-alternate-precedence":
return { requiresExercise: true, isExercisedBy: targetMatches };
case "response":
case "not-response":
case "chain-response":
case "not-chain-response":
case "alternate-response":
- case "not-alternate-response":
case "responded-existence":
case "not-responded-existence":
return { requiresExercise: true, isExercisedBy: activationMatches };
@@ -290,7 +251,6 @@ function createExercisePolicy(constraint: DeclareConstraint): Pick<
case "chain-succession":
case "not-chain-succession":
case "alternate-succession":
- case "not-alternate-succession":
return { requiresExercise: true, isExercisedBy: eitherMatches };
}
}
diff --git a/frontend/src/graph/declarePrecedenceMonitors.test.ts b/frontend/src/graph/declarePrecedenceMonitors.test.ts
index a061547..0cedd8c 100644
--- a/frontend/src/graph/declarePrecedenceMonitors.test.ts
+++ b/frontend/src/graph/declarePrecedenceMonitors.test.ts
@@ -6,7 +6,6 @@ import type { DeclareTransition } from "./declarePredicates";
import {
createAlternatePrecedenceMonitor,
createChainPrecedenceMonitor,
- createNotAlternatePrecedenceMonitor,
createNotChainPrecedenceMonitor,
createNotPrecedenceMonitor,
createPrecedenceMonitor,
@@ -68,7 +67,6 @@ const B = (id: number): DeclareTransition => ({
outputs: { id },
});
const X: DeclareTransition = { transition: "X" };
-const C: DeclareTransition = { transition: "C" };
describe("Precedence", () => {
it("is vacuously satisfied when no target occurs", () => {
@@ -160,36 +158,20 @@ describe("Chain precedence", () => {
});
describe("Alternate precedence", () => {
- it("requires an activation since the previous target", () => {
- const monitor = createAlternatePrecedenceMonitor(
- group("A"),
- group("B"),
- group("C"),
- );
+ it("allows unrelated events and requires a fresh activation after the previous target", () => {
+ const monitor = createAlternatePrecedenceMonitor(group("A"), group("B"));
expect(status(monitor, [{ transition: "A" }, X, { transition: "B" }]).accepting).toBe(true);
expect(status(monitor, [{ transition: "A" }, { transition: "B" }, { transition: "B" }])).toEqual({
viable: false,
accepting: false,
});
+ expect(status(monitor, [{ transition: "A" }, { transition: "B" }, { transition: "A" }, { transition: "B" }]).accepting).toBe(true);
});
- it("rejects the configured between predicate after the activation", () => {
- const monitor = createAlternatePrecedenceMonitor(
- group("A"),
- group("B"),
- group("C"),
- );
- expect(status(monitor, [{ transition: "A" }, C, { transition: "B" }])).toEqual({
- viable: false,
- accepting: false,
- });
- });
-
- it("uses correlation for the preceding activation", () => {
+ it("uses a correlated activation since the previous target", () => {
const monitor = createAlternatePrecedenceMonitor(
correlatedActivation,
group("B"),
- group("C"),
correlation,
);
expect(status(monitor, [A(10), B(10)]).accepting).toBe(true);
@@ -199,32 +181,3 @@ describe("Alternate precedence", () => {
});
});
});
-
-describe("Specialized negative alternate precedence", () => {
- it("forbids A then B when only the allowed C predicate occurs between", () => {
- const monitor = createNotAlternatePrecedenceMonitor(
- group("A"),
- group("B"),
- group("C"),
- );
- expect(status(monitor, [{ transition: "A" }, C, { transition: "B" }])).toEqual({
- viable: false,
- accepting: false,
- });
- expect(status(monitor, [{ transition: "A" }, X, { transition: "B" }]).accepting).toBe(true);
- });
-
- it("applies correlation to the forbidden preceding activation", () => {
- const monitor = createNotAlternatePrecedenceMonitor(
- correlatedActivation,
- group("B"),
- group("C"),
- correlation,
- );
- expect(status(monitor, [A(10), C, B(20)]).accepting).toBe(true);
- expect(status(monitor, [A(10), C, B(10)])).toEqual({
- viable: false,
- accepting: false,
- });
- });
-});
diff --git a/frontend/src/graph/declarePrecedenceMonitors.ts b/frontend/src/graph/declarePrecedenceMonitors.ts
index cabc833..7b9f682 100644
--- a/frontend/src/graph/declarePrecedenceMonitors.ts
+++ b/frontend/src/graph/declarePrecedenceMonitors.ts
@@ -29,7 +29,6 @@ export type ChainPrecedenceMonitorState = {
export type AlternatePrecedenceMonitorState = {
candidateActivations: SeenActivation[];
- blocked: boolean;
violated: boolean;
};
@@ -207,112 +206,34 @@ export function createNotChainPrecedenceMonitor(
export function createAlternatePrecedenceMonitor(
activation: DeclarePredicateGroup,
target: DeclarePredicateGroup,
- between: DeclarePredicateGroup,
correlation?: CorrelationCondition,
): DeclareMonitor {
return {
- initialState: () => ({
- candidateActivations: [],
- blocked: false,
- violated: false,
- }),
+ initialState: () => ({ candidateActivations: [], violated: false }),
advance: (state, edge) => {
- if (state.violated) {
- return state;
- }
+ if (state.violated) return state;
const targetOccurs = groupMatches(target, edge);
- if (targetOccurs) {
- const fulfilled =
- !state.blocked &&
- hasCorrelatedActivation(
- state.candidateActivations,
- correlation,
- edge,
- );
- return {
- candidateActivations: activationMatches(activation, edge),
- blocked: false,
- violated: !fulfilled,
- };
- }
-
const newActivations = activationMatches(activation, edge);
- if (newActivations.length > 0) {
- return {
- candidateActivations: newActivations,
- blocked: false,
- violated: false,
- };
- }
-
- if (
- state.candidateActivations.length > 0 &&
- groupMatches(between, edge)
- ) {
- return { ...state, blocked: true };
- }
-
- return state;
- },
- status: (state) => ({
- viable: !state.violated,
- accepting: !state.violated,
- }),
- stateKey: canonicalMonitorStateKey,
- };
-}
-
-export function createNotAlternatePrecedenceMonitor(
- activation: DeclarePredicateGroup,
- target: DeclarePredicateGroup,
- allowedBetween: DeclarePredicateGroup,
- correlation?: CorrelationCondition,
-): DeclareMonitor {
- return {
- initialState: () => ({
- candidateActivations: [],
- blocked: false,
- violated: false,
- }),
- advance: (state, edge) => {
- if (state.violated) {
- return state;
- }
-
- const targetOccurs = groupMatches(target, edge);
if (targetOccurs) {
- const forbiddenSequence =
- !state.blocked &&
- hasCorrelatedActivation(
- state.candidateActivations,
- correlation,
- edge,
- );
- return {
- candidateActivations: activationMatches(activation, edge),
- blocked: false,
- violated: forbiddenSequence,
- };
- }
-
- const newActivations = activationMatches(activation, edge);
- if (newActivations.length > 0) {
+ const fulfilled = hasCorrelatedActivation(
+ state.candidateActivations,
+ correlation,
+ edge,
+ );
return {
candidateActivations: newActivations,
- blocked: false,
- violated: false,
+ violated: !fulfilled,
};
}
- if (
- state.candidateActivations.length > 0 &&
- !groupMatches(allowedBetween, edge)
- ) {
- return { ...state, blocked: true };
- }
-
- return state;
+ return {
+ candidateActivations: [
+ ...state.candidateActivations,
+ ...newActivations,
+ ],
+ violated: false,
+ };
},
status: (state) => ({
viable: !state.violated,
diff --git a/frontend/src/graph/declareResponseMonitors.test.ts b/frontend/src/graph/declareResponseMonitors.test.ts
index fbd8e08..23a99e5 100644
--- a/frontend/src/graph/declareResponseMonitors.test.ts
+++ b/frontend/src/graph/declareResponseMonitors.test.ts
@@ -6,7 +6,6 @@ import type { DeclareTransition } from "./declarePredicates";
import {
createAlternateResponseMonitor,
createChainResponseMonitor,
- createNotAlternateResponseMonitor,
createNotChainResponseMonitor,
createNotResponseMonitor,
createResponseMonitor,
@@ -64,7 +63,6 @@ const B = (id: number): DeclareTransition => ({
outputs: { id },
});
const X: DeclareTransition = { transition: "X" };
-const C: DeclareTransition = { transition: "C" };
describe("Response", () => {
it("is vacuously satisfied without activations", () => {
@@ -147,62 +145,42 @@ describe("Chain response", () => {
});
describe("Alternate response", () => {
- it("requires a target before another activation", () => {
- const monitor = createAlternateResponseMonitor(
- group("A"),
- group("B"),
- group("C"),
- );
+ it("allows unrelated events but rejects a second qualifying activation before the target", () => {
+ const monitor = createAlternateResponseMonitor(group("A"), group("B"));
expect(status(monitor, [{ transition: "A" }, X, { transition: "B" }]).accepting).toBe(true);
- expect(status(monitor, [{ transition: "A" }, { transition: "A" }])).toEqual({
+ expect(status(monitor, [{ transition: "A" }, { transition: "A" }, { transition: "B" }])).toEqual({
viable: false,
accepting: false,
});
});
- it("rejects the configured between predicate while waiting", () => {
- const monitor = createAlternateResponseMonitor(
- group("A"),
- group("B"),
- group("C"),
- );
- expect(status(monitor, [{ transition: "A" }, C])).toEqual({
- viable: false,
- accepting: false,
- });
+ it("uses the activation condition to decide whether a repeated activity qualifies", () => {
+ const activation = {
+ relation: "or" as const,
+ predicates: [{
+ transition: { operator: "equals" as const, value: "A" },
+ condition: {
+ type: "source" as const,
+ source: "inputs" as const,
+ condition: { type: "comparison" as const, path: ["qualifies"], operator: "=" as const, value: true },
+ },
+ }],
+ };
+ const monitor = createAlternateResponseMonitor(activation, group("B"));
+ expect(status(monitor, [
+ { transition: "A", inputs: { qualifies: true } },
+ { transition: "A", inputs: { qualifies: false } },
+ { transition: "B" },
+ ]).accepting).toBe(true);
});
- it("uses target correlation before fulfilling the activation", () => {
+ it("requires a correlated target", () => {
const monitor = createAlternateResponseMonitor(
correlatedActivation,
group("B"),
- group("C"),
correlation,
);
expect(status(monitor, [A(10), B(20)]).accepting).toBe(false);
expect(status(monitor, [A(10), B(10)]).accepting).toBe(true);
});
});
-
-describe("Specialized negative alternate response", () => {
- it("rejects A followed by B with only the allowed C predicate between", () => {
- const monitor = createNotAlternateResponseMonitor(
- group("A"),
- group("B"),
- group("C"),
- );
- expect(status(monitor, [{ transition: "A" }, C, { transition: "B" }]).accepting).toBe(false);
- expect(status(monitor, [{ transition: "A" }, X, { transition: "B" }]).accepting).toBe(true);
- });
-
- it("applies correlation to the forbidden target", () => {
- const monitor = createNotAlternateResponseMonitor(
- correlatedActivation,
- group("B"),
- group("C"),
- correlation,
- );
- expect(status(monitor, [A(10), C, B(20)]).accepting).toBe(true);
- expect(status(monitor, [A(10), C, B(10)]).accepting).toBe(false);
- });
-});
diff --git a/frontend/src/graph/declareResponseMonitors.ts b/frontend/src/graph/declareResponseMonitors.ts
index 8d194bd..9fd5039 100644
--- a/frontend/src/graph/declareResponseMonitors.ts
+++ b/frontend/src/graph/declareResponseMonitors.ts
@@ -196,123 +196,32 @@ export function createNotChainResponseMonitor(
export function createAlternateResponseMonitor(
activation: DeclarePredicateGroup,
target: DeclarePredicateGroup,
- between: DeclarePredicateGroup,
correlation?: CorrelationCondition,
): DeclareMonitor {
return {
- initialState: () => ({
- pending: null,
- possibleTargets: [],
- violated: false,
- }),
+ initialState: () => ({ pending: null, possibleTargets: [], violated: false }),
advance: (state, edge) => {
- if (state.violated) {
- return state;
- }
+ if (state.violated) return state;
- const newActivations = activationMatches(activation, edge);
- if (newActivations.length > 0) {
- const fulfilled =
- state.pending === null ||
- state.possibleTargets.some((candidate) =>
- targetCorrelates(target, correlation, state.pending!, candidate),
- );
- return {
- pending: newActivations[0],
- possibleTargets: [],
- violated: !fulfilled,
- };
- }
-
- if (state.pending !== null && groupMatches(between, edge)) {
- return { ...state, violated: true };
- }
-
- return state.pending !== null && groupMatches(target, edge)
- ? {
- ...state,
- possibleTargets: [...state.possibleTargets, edge],
- }
- : state;
- },
- status: (state) => {
- const pendingFulfilled =
- state.pending === null ||
- state.possibleTargets.some((candidate) =>
- targetCorrelates(target, correlation, state.pending!, candidate),
- );
- return {
- viable: !state.violated,
- accepting: !state.violated && pendingFulfilled,
- };
- },
- stateKey: canonicalMonitorStateKey,
- };
-}
-
-export function createNotAlternateResponseMonitor(
- activation: DeclarePredicateGroup,
- target: DeclarePredicateGroup,
- allowedBetween: DeclarePredicateGroup,
- correlation?: CorrelationCondition,
-): DeclareMonitor {
- return {
- initialState: () => ({
- pending: null,
- possibleTargets: [],
- violated: false,
- }),
- advance: (state, edge) => {
- if (state.violated) {
- return state;
+ let pending = state.pending;
+ if (pending !== null && targetCorrelates(target, correlation, pending, edge)) {
+ pending = null;
}
const newActivations = activationMatches(activation, edge);
if (newActivations.length > 0) {
- const forbiddenSequenceCompleted =
- state.pending !== null &&
- state.possibleTargets.some((candidate) =>
- targetCorrelates(target, correlation, state.pending!, candidate),
- );
- return {
- pending: newActivations[0],
- possibleTargets: [],
- violated: forbiddenSequenceCompleted,
- };
- }
-
- if (state.pending === null) {
- return state;
- }
-
- if (groupMatches(target, edge)) {
- return {
- ...state,
- possibleTargets: [...state.possibleTargets, edge],
- };
+ if (pending !== null) {
+ return { pending, possibleTargets: [], violated: true };
+ }
+ pending = newActivations[0];
}
- if (!groupMatches(allowedBetween, edge)) {
- return {
- pending: null,
- possibleTargets: [],
- violated: false,
- };
- }
-
- return state;
- },
- status: (state) => {
- const forbiddenSequenceCompleted =
- state.pending !== null &&
- state.possibleTargets.some((candidate) =>
- targetCorrelates(target, correlation, state.pending!, candidate),
- );
- return {
- viable: !state.violated,
- accepting: !state.violated && !forbiddenSequenceCompleted,
- };
+ return { pending, possibleTargets: [], violated: false };
},
+ status: (state) => ({
+ viable: !state.violated,
+ accepting: !state.violated && state.pending === null,
+ }),
stateKey: canonicalMonitorStateKey,
};
}
diff --git a/frontend/src/graph/declareSuccessionMonitors.test.ts b/frontend/src/graph/declareSuccessionMonitors.test.ts
index 2289e5b..b3370d8 100644
--- a/frontend/src/graph/declareSuccessionMonitors.test.ts
+++ b/frontend/src/graph/declareSuccessionMonitors.test.ts
@@ -6,7 +6,6 @@ import type { DeclareTransition } from "./declarePredicates";
import {
createAlternateSuccessionMonitor,
createChainSuccessionMonitor,
- createNotAlternateSuccessionMonitor,
createNotChainSuccessionMonitor,
createNotSuccessionMonitor,
createSuccessionMonitor,
@@ -68,7 +67,6 @@ const B = (id: number): DeclareTransition => ({
outputs: { id },
});
const X: DeclareTransition = { transition: "X" };
-const C: DeclareTransition = { transition: "C" };
describe("Succession", () => {
it("combines response and precedence semantics", () => {
@@ -143,17 +141,13 @@ describe("Chain succession", () => {
});
describe("Alternate succession", () => {
- it("combines alternate response and alternate precedence", () => {
- const monitor = createAlternateSuccessionMonitor(
- group("A"),
- group("B"),
- group("C"),
- );
+ it("combines standard alternate response and alternate precedence", () => {
+ const monitor = createAlternateSuccessionMonitor(group("A"), group("B"));
expect(status(monitor, [{ transition: "A" }, X, { transition: "B" }])).toEqual({
viable: true,
accepting: true,
});
- expect(status(monitor, [{ transition: "A" }, { transition: "A" }])).toEqual({
+ expect(status(monitor, [{ transition: "A" }, { transition: "A" }, { transition: "B" }])).toEqual({
viable: false,
accepting: false,
});
@@ -161,30 +155,13 @@ describe("Alternate succession", () => {
viable: false,
accepting: false,
});
- expect(status(monitor, [{ transition: "A" }, C, { transition: "B" }])).toEqual({
- viable: false,
- accepting: false,
- });
- });
-
- it("implements specialized negative alternate succession", () => {
- const monitor = createNotAlternateSuccessionMonitor(
- group("A"),
- group("B"),
- group("C"),
- );
- expect(status(monitor, [{ transition: "A" }, C, { transition: "B" }])).toEqual({
- viable: false,
- accepting: false,
- });
- expect(status(monitor, [{ transition: "A" }, X, { transition: "B" }]).accepting).toBe(true);
+ expect(status(monitor, [{ transition: "A" }, { transition: "B" }, { transition: "A" }, { transition: "B" }]).accepting).toBe(true);
});
- it("preserves correlation in the composed alternate monitors", () => {
+ it("preserves correlation in both composed directions", () => {
const monitor = createAlternateSuccessionMonitor(
correlatedActivation,
group("B"),
- group("C"),
correlation,
);
expect(status(monitor, [A(10), B(10)]).accepting).toBe(true);
diff --git a/frontend/src/graph/declareSuccessionMonitors.ts b/frontend/src/graph/declareSuccessionMonitors.ts
index 6fe55b7..a642a12 100644
--- a/frontend/src/graph/declareSuccessionMonitors.ts
+++ b/frontend/src/graph/declareSuccessionMonitors.ts
@@ -7,7 +7,6 @@ import type { DeclareTransition } from "./declarePredicates";
import {
createAlternatePrecedenceMonitor,
createChainPrecedenceMonitor,
- createNotAlternatePrecedenceMonitor,
createNotChainPrecedenceMonitor,
createNotPrecedenceMonitor,
createPrecedenceMonitor,
@@ -15,7 +14,6 @@ import {
import {
createAlternateResponseMonitor,
createChainResponseMonitor,
- createNotAlternateResponseMonitor,
createNotChainResponseMonitor,
createNotResponseMonitor,
createResponseMonitor,
@@ -99,43 +97,10 @@ export function createNotChainSuccessionMonitor(
export function createAlternateSuccessionMonitor(
activation: DeclarePredicateGroup,
target: DeclarePredicateGroup,
- between: DeclarePredicateGroup,
correlation?: CorrelationCondition,
): DeclareMonitor {
return composeMonitors(
- createAlternateResponseMonitor(
- activation,
- target,
- between,
- correlation,
- ),
- createAlternatePrecedenceMonitor(
- activation,
- target,
- between,
- correlation,
- ),
- );
-}
-
-export function createNotAlternateSuccessionMonitor(
- activation: DeclarePredicateGroup,
- target: DeclarePredicateGroup,
- allowedBetween: DeclarePredicateGroup,
- correlation?: CorrelationCondition,
-): DeclareMonitor {
- return composeMonitors(
- createNotAlternateResponseMonitor(
- activation,
- target,
- allowedBetween,
- correlation,
- ),
- createNotAlternatePrecedenceMonitor(
- activation,
- target,
- allowedBetween,
- correlation,
- ),
+ createAlternateResponseMonitor(activation, target, correlation),
+ createAlternatePrecedenceMonitor(activation, target, correlation),
);
}
diff --git a/frontend/src/graph/graphJson.test.ts b/frontend/src/graph/graphJson.test.ts
index 84c49b3..2dd9c55 100644
--- a/frontend/src/graph/graphJson.test.ts
+++ b/frontend/src/graph/graphJson.test.ts
@@ -441,3 +441,164 @@ 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([]);
+ });
+});
+
+describe("path-search configuration persistence", () => {
+ const targetSearch = {
+ sourceNodeId: "0",
+ endpointMode: "specific-target" as const,
+ targetNodeId: "2",
+ requestedPathCount: 17,
+ maximumVisitsPerState: 3,
+ requireConstraintExercise: false,
+ };
+
+ it("round-trips target-specific search settings", () => {
+ const document = createGraphJsonDocument(
+ graph,
+ undefined,
+ [],
+ targetSearch,
+ );
+ const reparsed = parseGraphJsonText(serializeGraphJson(document));
+ expect(reparsed.pathSearch).toEqual(targetSearch);
+ expect(reparsed.document.pathSearch).toEqual(targetSearch);
+ });
+
+ it("round-trips constraint-satisfaction settings without a target", () => {
+ const pathSearch = {
+ sourceNodeId: "1",
+ endpointMode: "constraint-satisfaction" as const,
+ requestedPathCount: 7,
+ maximumVisitsPerState: 2,
+ requireConstraintExercise: true,
+ };
+ const document = createGraphJsonDocument(graph, undefined, [], pathSearch);
+ expect(
+ parseGraphJsonText(serializeGraphJson(document)).pathSearch,
+ ).toEqual(pathSearch);
+ });
+
+ it("reads older documents without search settings", () => {
+ const result = parseGraphJsonValue({
+ nodes: graph.nodes,
+ edges: graph.edges,
+ });
+ expect(result.pathSearch).toBeNull();
+ expect(result.document).not.toHaveProperty("pathSearch");
+ });
+
+ it("rejects invalid modes, counts, and endpoint combinations", () => {
+ const base = { nodes: graph.nodes, edges: graph.edges };
+ expect(() =>
+ parseGraphJsonValue({
+ ...base,
+ pathSearch: { ...targetSearch, endpointMode: "other" },
+ }),
+ ).toThrow(/pathSearch\.endpointMode/);
+ expect(() =>
+ parseGraphJsonValue({
+ ...base,
+ pathSearch: { ...targetSearch, requestedPathCount: 0 },
+ }),
+ ).toThrow(/requestedPathCount must be a positive integer/);
+ expect(() =>
+ parseGraphJsonValue({
+ ...base,
+ pathSearch: { ...targetSearch, maximumVisitsPerState: 0 },
+ }),
+ ).toThrow(/maximumVisitsPerState must be a positive integer/);
+ expect(() =>
+ parseGraphJsonValue({
+ ...base,
+ pathSearch: {
+ ...targetSearch,
+ endpointMode: "constraint-satisfaction",
+ },
+ }),
+ ).toThrow(/targetNodeId must be omitted/);
+ expect(() =>
+ parseGraphJsonValue({
+ ...base,
+ pathSearch: {
+ sourceNodeId: targetSearch.sourceNodeId,
+ endpointMode: targetSearch.endpointMode,
+ requestedPathCount: targetSearch.requestedPathCount,
+ maximumVisitsPerState: targetSearch.maximumVisitsPerState,
+ requireConstraintExercise: targetSearch.requireConstraintExercise,
+ },
+ }),
+ ).toThrow(/targetNodeId must be a non-empty string/);
+ });
+
+ it("rejects search settings that reference unknown graph states", () => {
+ const base = { nodes: graph.nodes, edges: graph.edges };
+ expect(() =>
+ parseGraphJsonValue({
+ ...base,
+ pathSearch: { ...targetSearch, sourceNodeId: "missing" },
+ }),
+ ).toThrow(/sourceNodeId references missing state missing/);
+ expect(() =>
+ parseGraphJsonValue({
+ ...base,
+ pathSearch: { ...targetSearch, targetNodeId: "missing" },
+ }),
+ ).toThrow(/targetNodeId references missing state missing/);
+ });
+});
diff --git a/frontend/src/graph/graphJson.ts b/frontend/src/graph/graphJson.ts
index e406b9e..845b851 100644
--- a/frontend/src/graph/graphJson.ts
+++ b/frontend/src/graph/graphJson.ts
@@ -1,3 +1,6 @@
+import type { DeclareConstraint } from "./declareConstraints";
+import type { PathSearchEndpointMode } from "./pathSearch";
+import { parseDeclareConstraintsJson } from "./declareConstraintJson";
import {
resolvePath,
type PathEdge,
@@ -30,6 +33,14 @@ export interface GraphJsonMetadata {
createdAt?: string;
[key: string]: unknown;
}
+export interface PersistedPathSearchConfiguration {
+ sourceNodeId: string;
+ endpointMode: PathSearchEndpointMode;
+ targetNodeId?: string;
+ requestedPathCount: number;
+ maximumVisitsPerState: number;
+ requireConstraintExercise: boolean;
+}
export interface GraphJsonDocument {
format: "ltsvisualizer";
@@ -38,6 +49,8 @@ export interface GraphJsonDocument {
metadata?: GraphJsonMetadata;
nodes: JsonGraphNode[];
edges: JsonGraphEdge[];
+ declareConstraints?: DeclareConstraint[];
+ pathSearch?: PersistedPathSearchConfiguration;
}
export interface SelectedPathJsonDocument {
@@ -53,6 +66,8 @@ export interface SelectedPathJsonDocument {
nodes: JsonGraphNode[];
edges: JsonGraphEdge[];
path: SelectedPath;
+ declareConstraints?: DeclareConstraint[];
+ pathSearch?: PersistedPathSearchConfiguration;
}
export type LtsVisualizerJsonDocument =
@@ -63,6 +78,8 @@ export interface ParsedGraphJson {
document: LtsVisualizerJsonDocument;
graph: JsonGraphData;
selectedPath: SelectedPath | null;
+ declareConstraints: DeclareConstraint[];
+ pathSearch: PersistedPathSearchConfiguration | null;
}
export class GraphJsonError extends Error {
@@ -225,6 +242,77 @@ function parseMetadata(value: unknown): GraphJsonMetadata | undefined {
}
return requireObject(value, "metadata") as GraphJsonMetadata;
}
+function requirePositiveInteger(value: unknown, label: string): number {
+ if (!Number.isInteger(value) || (value as number) < 1) {
+ throw new GraphJsonError(`${label} must be a positive integer.`);
+ }
+ return value as number;
+}
+function requireBoolean(value: unknown, label: string): boolean {
+ if (typeof value !== "boolean") {
+ throw new GraphJsonError(`${label} must be a boolean.`);
+ }
+ return value;
+}
+function parsePathSearchConfiguration(
+ value: unknown,
+ graph: JsonGraphData,
+): PersistedPathSearchConfiguration | undefined {
+ if (value === undefined) return undefined;
+ const configuration = requireObject(value, "pathSearch");
+ const sourceNodeId = requireString(
+ configuration.sourceNodeId,
+ "pathSearch.sourceNodeId",
+ );
+ const endpointMode = configuration.endpointMode;
+ if (
+ endpointMode !== "specific-target" &&
+ endpointMode !== "constraint-satisfaction"
+ ) {
+ throw new GraphJsonError(
+ 'pathSearch.endpointMode must be either "specific-target" or "constraint-satisfaction".',
+ );
+ }
+ const nodeIds = new Set(graph.nodes.map((node) => node.id));
+ if (!nodeIds.has(sourceNodeId)) {
+ throw new GraphJsonError(
+ `pathSearch.sourceNodeId references missing state ${sourceNodeId}.`,
+ );
+ }
+ let targetNodeId: string | undefined;
+ if (endpointMode === "specific-target") {
+ targetNodeId = requireString(
+ configuration.targetNodeId,
+ "pathSearch.targetNodeId",
+ );
+ if (!nodeIds.has(targetNodeId)) {
+ throw new GraphJsonError(
+ `pathSearch.targetNodeId references missing state ${targetNodeId}.`,
+ );
+ }
+ } else if (configuration.targetNodeId !== undefined) {
+ throw new GraphJsonError(
+ "pathSearch.targetNodeId must be omitted in constraint-satisfaction mode.",
+ );
+ }
+ return {
+ sourceNodeId,
+ endpointMode,
+ ...(targetNodeId ? { targetNodeId } : {}),
+ requestedPathCount: requirePositiveInteger(
+ configuration.requestedPathCount,
+ "pathSearch.requestedPathCount",
+ ),
+ maximumVisitsPerState: requirePositiveInteger(
+ configuration.maximumVisitsPerState,
+ "pathSearch.maximumVisitsPerState",
+ ),
+ requireConstraintExercise: requireBoolean(
+ configuration.requireConstraintExercise,
+ "pathSearch.requireConstraintExercise",
+ ),
+ };
+}
function normalizeDocument(value: unknown): LtsVisualizerJsonDocument {
const root = requireObject(value, "JSON root");
@@ -261,6 +349,11 @@ function normalizeDocument(value: unknown): LtsVisualizerJsonDocument {
? "selected-path"
: "graph";
const metadata = parseMetadata(root.metadata);
+ const declareConstraints =
+ root.declareConstraints === undefined
+ ? []
+ : parseDeclareConstraintsJson(root.declareConstraints);
+ const pathSearch = parsePathSearchConfiguration(root.pathSearch, graph);
if (type === "selected-path") {
const selectedPath = parseSelectedPath(root.path);
@@ -282,6 +375,8 @@ function normalizeDocument(value: unknown): LtsVisualizerJsonDocument {
nodes,
edges,
path: selectedPath,
+ ...(declareConstraints.length > 0 ? { declareConstraints } : {}),
+ ...(pathSearch ? { pathSearch } : {}),
};
}
@@ -292,6 +387,8 @@ function normalizeDocument(value: unknown): LtsVisualizerJsonDocument {
...(metadata ? { metadata } : {}),
nodes,
edges,
+ ...(declareConstraints.length > 0 ? { declareConstraints } : {}),
+ ...(pathSearch ? { pathSearch } : {}),
};
}
@@ -314,12 +411,16 @@ 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 ?? [],
+ pathSearch: document.pathSearch ?? null,
};
}
export function createGraphJsonDocument(
graph: JsonGraphData,
- metadata?: GraphJsonMetadata
+ metadata?: GraphJsonMetadata,
+ declareConstraints: readonly DeclareConstraint[] = [],
+ pathSearch?: PersistedPathSearchConfiguration,
): GraphJsonDocument {
return parseGraphJsonValue({
format: "ltsvisualizer",
@@ -332,13 +433,19 @@ export function createGraphJsonDocument(
},
nodes: graph.nodes,
edges: graph.edges,
+ ...(declareConstraints.length > 0
+ ? { declareConstraints: structuredClone(declareConstraints) }
+ : {}),
+ ...(pathSearch ? { pathSearch: structuredClone(pathSearch) } : {}),
}).document as GraphJsonDocument;
}
export function createSelectedPathJsonDocument(
graph: JsonGraphData,
path: SelectedPath,
- metadata?: GraphJsonMetadata
+ metadata?: GraphJsonMetadata,
+ declareConstraints: readonly DeclareConstraint[] = [],
+ pathSearch?: PersistedPathSearchConfiguration,
): SelectedPathJsonDocument {
const resolved = resolvePath(graph, path);
const selectedNodeIds = new Set(resolved.nodeIds);
@@ -362,6 +469,10 @@ export function createSelectedPathJsonDocument(
nodes: pathGraph.nodes,
edges: pathGraph.edges,
path,
+ ...(declareConstraints.length > 0
+ ? { declareConstraints: structuredClone(declareConstraints) }
+ : {}),
+ ...(pathSearch ? { pathSearch: structuredClone(pathSearch) } : {}),
}).document as SelectedPathJsonDocument;
}
diff --git a/frontend/src/graph/pathSearch.test.ts b/frontend/src/graph/pathSearch.test.ts
index ff95071..1aeaa02 100644
--- a/frontend/src/graph/pathSearch.test.ts
+++ b/frontend/src/graph/pathSearch.test.ts
@@ -23,6 +23,13 @@ function searchInput(
};
}
+function groupForTest(name: string) {
+ return {
+ relation: "or" as const,
+ predicates: [{ transition: { operator: "equals" as const, value: name } }],
+ };
+}
+
describe("findKShortestBoundedPaths", () => {
it("finds a direct path", () => {
const result = findKShortestBoundedPaths(
@@ -592,13 +599,52 @@ 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 target-specific paths when exercise is required", () => {
+ const result = findKShortestBoundedPaths({
+ nodeIds: ["source", "target"],
+ edges: [
+ { id: "x", source: "source", target: "target", transition: "X" },
+ ],
+ sourceNodeId: "source",
+ targetNodeId: "target",
+ endpointMode: "specific-target",
+ requireConstraintExercise: true,
+ requestedPathCount: 1,
+ maximumVisitsPerState: 1,
+ constraints: { declare: [responseConstraint] },
+ });
+
+ expect(result.paths).toEqual([]);
+ });
+
+ it("allows vacuous target-specific paths when exercise is disabled", () => {
+ const result = findKShortestBoundedPaths({
+ nodeIds: ["source", "target"],
+ edges: [
+ { id: "x", source: "source", target: "target", transition: "X" },
+ ],
+ sourceNodeId: "source",
+ targetNodeId: "target",
+ endpointMode: "specific-target",
+ requireConstraintExercise: false,
+ requestedPathCount: 1,
+ maximumVisitsPerState: 1,
+ constraints: { declare: [responseConstraint] },
+ });
+
+ expect(result.paths).toHaveLength(1);
+ expect(result.paths[0]).toMatchObject({
+ startNodeId: "source",
+ edgeIds: ["x"],
+ });
});
it("rejects vacuous Response satisfaction when exercise is required", () => {
@@ -632,9 +678,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 +727,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 +767,194 @@ 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.",
+ });
+ });
+
+ it("uses standard Alternate Response semantics during path search", () => {
+ const result = findKShortestBoundedPaths(searchInput(
+ ["0", "1", "2", "3", "4"],
+ [
+ { id: "a", source: "0", target: "1", transition: "A" },
+ { id: "x", source: "1", target: "2", transition: "X" },
+ { id: "b", source: "2", target: "4", transition: "B" },
+ { id: "a-again", source: "1", target: "3", transition: "A" },
+ { id: "b-late", source: "3", target: "4", transition: "B" },
+ ],
+ {
+ requestedPathCount: 5,
+ constraints: { declare: [{
+ id: "alternate-response",
+ template: "alternate-response",
+ enabled: true,
+ activation: groupForTest("A"),
+ target: groupForTest("B"),
+ }] },
+ },
+ ));
+ expect(result.paths.map((path) => path.edgeIds)).toEqual([["a", "x", "b"]]);
+ });
+
+ it("uses standard Alternate Precedence semantics during path search", () => {
+ const result = findKShortestBoundedPaths(searchInput(
+ ["0", "1", "2", "3", "4", "5"],
+ [
+ { id: "a", source: "0", target: "1", transition: "A" },
+ { id: "x", source: "1", target: "2", transition: "X" },
+ { id: "b", source: "2", target: "5", transition: "B" },
+ { id: "b-first", source: "1", target: "3", transition: "B" },
+ { id: "x2", source: "3", target: "4", transition: "X" },
+ { id: "b-second", source: "4", target: "5", transition: "B" },
+ ],
+ {
+ requestedPathCount: 5,
+ constraints: { declare: [{
+ id: "alternate-precedence",
+ template: "alternate-precedence",
+ enabled: true,
+ activation: groupForTest("A"),
+ target: groupForTest("B"),
+ }] },
+ },
+ ));
+ expect(result.paths.map((path) => path.edgeIds)).toEqual([["a", "x", "b"]]);
+ });
+
+ it("uses both standard Alternate Succession directions during path search", () => {
+ const result = findKShortestBoundedPaths(searchInput(
+ ["0", "1", "2", "3", "4", "5"],
+ [
+ { id: "a", source: "0", target: "1", transition: "A" },
+ { id: "x", source: "1", target: "2", transition: "X" },
+ { id: "b", source: "2", target: "5", transition: "B" },
+ { id: "b-first", source: "1", target: "3", transition: "B" },
+ { id: "x2", source: "3", target: "4", transition: "X" },
+ { id: "b-second", source: "4", target: "5", transition: "B" },
+ ],
+ {
+ requestedPathCount: 5,
+ constraints: { declare: [{
+ id: "alternate-succession",
+ template: "alternate-succession",
+ enabled: true,
+ activation: groupForTest("A"),
+ target: groupForTest("B"),
+ }] },
+ },
+ ));
+ expect(result.paths.map((path) => path.edgeIds)).toEqual([["a", "x", "b"]]);
+ });
+
});
diff --git a/frontend/src/graph/pathSearch.ts b/frontend/src/graph/pathSearch.ts
index 9c8302e..90b193c 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,197 @@ 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 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;
+ return orderOkay && chainOkay &&
+ 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;
+ return orderOkay && chainOkay &&
+ 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-precedence":
+ case "not-chain-precedence":
+ case "not-responded-existence":
+ case "not-coexistence":
+ case "not-succession":
+ case "not-chain-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,13 +627,11 @@ 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" &&
- (input.requireConstraintExercise ?? true);
+ const requireConstraintExercise = input.requireConstraintExercise ?? true;
if (
endpointMode === "constraint-satisfaction" &&
@@ -497,6 +712,16 @@ export function findKShortestBoundedPaths(
? { endNodeId: candidate.currentNodeId }
: {}),
edgeIds,
+ ...(compiledConstraints.length > 0
+ ? {
+ explanations: explainAcceptedPath(
+ edgeIds,
+ edgesById,
+ declareConstraints,
+ compiledConstraints,
+ ),
+ }
+ : {}),
});
}