Add explainable, persistable Declare constraints to path search

[dbera]

Summary

Adds data-aware Declare constraints to bounded path search, persists the
constraints and search configuration in LTSVisualizer graph JSON, and explains
why each returned path satisfies the enabled constraints.

Constraint monitors remain the source of truth for path pruning and acceptance.
Explanations are reconstructed only for accepted paths, avoiding explanation
history on every queued search candidate.

What changed

Data-aware Declare constraints

• Add a Declare constraint builder to bounded path search.
• Support transition-label and nested input/output data predicates.
• Support activation-value captures and activation-target correlation.
• Support 27 templates across:
  • cardinality and position;
  • choice and existence;
  • response;
  • precedence;
  • succession.
• Validate constraints before path generation.

Standard Alternate semantics

Align the positive Alternate family with standard Declare/MP-Declare semantics:

• Alternate Response: every qualifying activation must receive a correlated
  later target before another qualifying activation occurs.
• Alternate Precedence: every qualifying target must have a correlated
  activation since the previous qualifying target.
• Alternate Succession: combines both directions.
• Unrelated transitions are allowed between activation and target.
• A same-label transition interrupts alternation only when its data condition
  also matches.

The former non-standard between operand and the following unsupported
negative variants were removed:

• Not Alternate Response
• Not Alternate Precedence
• Not Alternate Succession

Constrained path search

• Compile enabled Declare constraints into incremental monitors.
• Prune candidates when a constraint can no longer be satisfied.
• Accept paths only when all enabled constraints are accepting.
• Optionally require applicable constraints to be exercised.
• Apply exercise checking consistently to:
  • searches toward a target state;
  • target-free constraint-satisfaction searches.
• Preserve K-shortest ordering, bounded visits, cancellation, and resource
  limits.

Explainability

• Attach structured explanations to accepted paths.
• Show:
  • constraint ID and template;
  • satisfaction summary;
  • exercised or vacuous status;
  • supporting transition events;
  • one-based step numbers and edge IDs.
• Make evidence events clickable to focus the corresponding graph edge and
  display its transition data in the inspector.
• Generate explanations only after acceptance, without adding explanation
  history to queued search candidates.

Persistence

Persist and restore:

• Declare constraints;
• source state;
• endpoint mode;
• optional target state;
• requested path count;
• visits per state;
• exercise requirement.

Computed paths and explanations are not persisted. Rerunning the search
reconstructs them from the restored configuration.

Imported data is validated for:

• template IDs;
• nested predicates;
• captures and correlations;
• duplicate constraint IDs;
• graph-state references;
• endpoint combinations;
• path counts and visit limits.

Validation

Automated:

• Declare monitor tests
• Template registry and monitor factory tests
• Path-search integration tests
• Full unit-test suite
• Lint
• Standard Vite build
• Offline single-file build

Manual validation using the multidimensional-array graph:

• All 27 remaining templates covered through focused scenarios
• Nested multidimensional predicates
• Standard Alternate Response behavior
• Standard Alternate Precedence behavior
• Standard Alternate Succession behavior
• Target-specific exercise enforcement
• Vacuous satisfaction when exercise checking is disabled
• Multiple constraints and disabled constraints
• Explanation expansion and edge focusing
• Graph JSON export/import round trip

Notes

• Quantitative time conditions from full MP-Declare are outside this change.
• Monitor evaluation remains authoritative for path acceptance.
• Explanation generation does not affect search-state expansion.
• More detailed evidence for some specialized templates can be added
  independently in future work.