Add explainable, persistable Declare constraints to path search

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; }

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() {
                               >
                                 <span>Cyclic component {getCyclicComponentNumber(component.id)}</span>
                                 <small>
-                                  {component.nodeIds.length} states ·{" "}
+                                  {component.nodeIds.length} states{" \u00b7 "}
                                   {component.internalEdgeIds.length} transitions
                                 </small>
                               </button>
@@ -2325,8 +2365,9 @@ function App() {
                     </label>
                     <p className="path-search-help">
                       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.
                     </p>
                     <div className="path-search-number-row">
                       <div>
@@ -2386,13 +2427,53 @@ function App() {
                                   <small>
                                     {path.edgeIds.length} transition
                                     {path.edgeIds.length === 1 ? "" : "s"}
-                                    {` · Ends at state ${
+                                    {` \u00b7 Ends at state ${
                                       path.endNodeId ??
                                       steps.at(-1)?.target ??
                                       path.startNodeId
                                     }`}
                                   </small>
                                 </button>
+                                {(path.explanations?.length ?? 0) > 0 && (
+                                  <details className="computed-path-explanations">
+                                    <summary>Why this path satisfies the constraints</summary>
+                                    <div className="constraint-explanation-list">
+                                      {path.explanations?.map((explanation) => (
+                                        <section
+                                          key={explanation.constraintId}
+                                          className="constraint-explanation"
+                                        >
+                                          <div className="constraint-explanation-heading">
+                                            <strong>{explanation.constraintId}</strong>
+                                            <span>Satisfied</span>
+                                          </div>
+                                          <small>{explanation.template}</small>
+                                          <p>{explanation.summary}</p>
+                                          <p className="constraint-exercise-status">
+                                            {explanation.exercised
+                                              ? "Constraint was exercised by this path."
+                                              : "Constraint was satisfied without an exercise event."}
+                                          </p>
+                                          {explanation.events.length > 0 && (
+                                            <ol>
+                                              {explanation.events.map((explanationEvent, eventIndex) => (
+                                                <li key={`${explanationEvent.role}-${explanationEvent.stepNumber}-${explanationEvent.edgeId}-${eventIndex}`}>
+                                                  <button
+                                                    type="button"
+                                                    onClick={() => focusExplanationEvent(explanationEvent, index)}
+                                                  >
+                                                    {explanationEvent.role}: step {explanationEvent.stepNumber}{" "}
+                                                    {explanationEvent.transition} ({explanationEvent.edgeId})
+                                                  </button>
+                                                </li>
+                                              ))}
+                                            </ol>
+                                          )}
+                                        </section>
+                                      ))}
+                                    </div>
+                                  </details>
+                                )}
                                 <details className="computed-path-details">
                                   <summary>Show transition details</summary>
                                   {steps.length === 0 ? (
@@ -2432,7 +2513,7 @@ function App() {
                                             >
                                               {step.source}
                                             </button>
-                                            <span aria-hidden="true">→</span>
+                                            <span aria-hidden="true">{"\u2192"}</span>
                                             <button
                                               type="button"
                                               onClick={() =>

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") && (
-                  <>
-                    <TransitionPicker
-                      label="Between transition"
-                      value={transitionValue(constraint, "between")}
-                      options={transitionOptions}
-                      disabled={disabled}
-                      onChange={(value) =>
-                        changeTransition(constraint.id, "between", value)
-                      }
-                    />
-                    <TransitionConditionEditor
-                  catalogue={transitionDataCatalogue}
-                  transitionName={transitionValue(constraint, "between")}
-                  condition={transitionCondition(constraint, "between")}
-                  disabled={disabled}
-                  onChange={(condition) =>
-                    changeCondition(constraint.id, "between", condition)
-                  }
-                />
-                  </>
-                )}
                 {definition.supportsCount && (
                   <label>
                     Count N

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/);
+  });
+});