nfa: +refactor Compute useful states with two reachability passes

[Adda0]

Replace the Tarjan-based implementation of get_useful_states() with a simpler and faster two-pass algorithm: a forward reachability pass from initial states, followed by a backward BFS from final states over a predecessor CSR (compressed sparse row) index. The new implementation:

• Adds a label-free predecessor CSR index with a source filter to only index forward-reachable transitions
• Implements forward reachability from a custom initial set
• Walks backward over predecessors to find all useful states
• Honors custom initial and final sets for noodlification use cases

LOCAL BENCHMARK (Release build, 1M-state DAG with 2M transitions):

• Old Tarjan-based: 22.2 ms/iter
• New two-pass: 8.8 ms/iter
• Speedup: 2.52×

Keeps Tarjan in place for its remaining callers (is_acyclic, is_flat, tarjan_scc_discover).

Permanent test added: 'mata::nfa::get_useful_states() with brute-force oracle' validates correctness against an independent oracle on randomized graphs (50 test cases with 5-50 states and random edges) and verifies trim() state renamings.

Part of #786. Not included: the benchmark against the compact templated
Tarjan of #224 (b) and recording the decision in the issue (item 3), and the
optional sharing of the predecessor index through #811 (item 5).

[greptile-apps]

Confidence Score: 5/5

[Medium impact] The PR appears safe to merge; no actionable issues were found.

Summary

Replaces Tarjan in get_useful_states() with forward reachability and a backward walk through a predecessor index.

• Useful-state checks now find paths with two reachability walks.

Adda0 explicitly deferred the compact-Tarjan benchmark and decision record, and optional predecessor-index sharing.

Diagram

%%{init: {'theme': 'neutral'}}%%
flowchart LR
  A[Selected initial states] --> B[Find reachable states]
  B --> C[Index predecessors from reachable sources]
  D[Selected final states] --> E[Keep reachable final states]
  B --> E
  C --> F[Walk backward]
  E --> F
  F --> G[Useful states]

Loading

_{Reviews (1) · Last reviewed commit: "nfa: +refactor Compute useful states wit..." · Reviewed by Greptile}