Add generic any-witness strategy for constrained path search

[dbera]

Summary

This PR adds a generic Any witness (fast) strategy to bounded, Declare-constrained path search.

The existing Shortest paths strategy remains the default and preserves deterministic shortest-first behavior. The new strategy prioritizes candidates that have made greater progress toward satisfying and exercising the configured Declare constraints.

Users can request one or more witnesses. Any-witness results are returned in deterministic heuristic discovery order and are not guaranteed to be shortest.

Motivation

Shortest-first exploration can spend a large part of the candidate budget enumerating shallow prefixes that make little progress toward the configured constraints.

This is especially expensive for highly branching state spaces and target-free constrained searches, where finding any satisfying execution is often more useful than proving that the returned execution is shortest.

The new strategy provides a faster alternative without introducing graph- or model-specific knowledge.

Changes

Search strategy

• Added a PathSearchStrategy with:
  • shortest
  • any-witness
• Added a strategy selector to the Paths panel.
• Passed the selected strategy through the application and worker search input.
• Kept shortest as the default for backward compatibility.

Any-witness prioritization

Any-witness search prioritizes candidates using generic Declare-monitor progress:

1. More accepting constraints
2. More exercised constraints
3. More monitors advanced from their initial state
4. Shorter path depth
5. Earlier insertion order for deterministic tie-breaking

The heuristic does not contain model-specific transition names, data fields, or constraint assumptions.

Multiple witnesses

• Any-witness search now respects the user-selected Number of paths.
• The search returns up to the requested number of distinct satisfying paths.
• Results are returned in heuristic discovery order and are not guaranteed to be shortest.
• Search stops when:
  • the requested count is reached;
  • the bounded search space is exhausted;
  • the search is cancelled; or
  • an internal resource safeguard is reached.

Loop handling and path identity

• Both strategies use the existing Visits per state bound.
• A value of 1 produces loopless paths.
• Higher values allow bounded revisits and self-loops.
• Paths remain unique by ordered edge-ID sequence, preserving:
  • parallel-edge identity;
  • repeated transitions;
  • loops; and
  • exact traversal order.

Persistence and UI

• Persisted the selected strategy in complete-graph JSON exports.
• Preserved the user-selected requested path count for Any-witness searches.
• Older JSON documents without a strategy continue to use shortest.
• Updated help and status text to distinguish shortest-first results from heuristic witness discovery.

Documentation

• Updated the README and changelog to describe the new strategy, semantics, persistence, and limitations.

Performance observation

For the ThalesDemo constrained-search example:

• Shortest-style exploration reached 144,227 expanded candidates without finding a path before the resource limit.
• Any-witness search found a valid 27-transition path after 284 expanded candidates.

This is approximately a 508x reduction in expanded candidates for that example.

This result is an observation for the tested graph and constraints, not a general performance guarantee.

Compatibility

• Existing shortest-path behavior remains unchanged.
• The default strategy is shortest.
• Existing graph JSON files remain supported.
• The same candidate and queue safeguards apply to both strategies.
• Hosted and offline builds use the same search implementation.

Tests

Added focused coverage verifying that:

• Any-witness honors the requested path count.
• Search stops after reaching the requested count.
• Exhaustion is reported when fewer witnesses exist.
• Parallel-edge witnesses remain distinct by ordered edge ID.
• A loop-dependent witness is rejected with a visit limit of 1.
• The same witness is accepted with a visit limit of 2.
• Self-loops follow the configured visit bound.
• Any-witness results remain deterministic for identical input.
• Existing deterministic shortest-first behavior remains unchanged.

Validation completed:

• npm test
• npm run lint
• npm run build
• npm run build:offline

Focused path-search result:

• 48 tests passed
• 0 lint warnings
• 0 lint errors

Manual verification

• Any-witness strategy is passed to the actual worker search.
• ThalesDemo returns a valid constrained witness.
• Constraint explanations identify the matching path steps.
• Number of paths is editable in Any-witness mode.
• Requested witness count is preserved during graph export.
• Loop behavior remains controlled by Visits per state.
• Shortest paths remains available and unchanged.

Limitations

• Any-witness results are not guaranteed to be shortest.
• Requesting additional witnesses may require substantially more time and memory than finding the first witness.
• Highly connected graphs can still reach the internal expanded- or queued-candidate safeguards.
• No prefix/product-state dominance pruning is introduced in this PR.