Add R2P support with benchmarks and reorganize into R2R/R2P

[avitalpresearch-droid]

Latest: Refactor R2P alive region, fix strategy reach phase, add NoC benchmarks

1. Refactor: Extract ComputeR2PAliveRegion shared method
Steps 1–5 of the R2P algorithm (build joint demanded predicate, compute state-dependent alive region) were duplicated in ComputeCoveredRegion and ComputeCycleStrategy. Extracted into a single ComputeR2PAliveRegion method that both call.

2. Fix: AND → OR in ComputeR2PPathStrategy realizable region
The two-phase R2P path strategy (reach alive, then maintain) had its realizable region computed as reach & maintain. Since maintain is only realizable at alive states, the AND collapsed to just alive — making the reach phase dead code. The cycle strategy would never activate it from states outside alive, falling back to idle instead of driving toward alive. Changed to OR so both phases contribute.

Verified via --play: with AND, the system stays at (x=0, y=0) forever (idle, FG(y) violated); with OR, it reaches (x=0, y=1) by step 2 and stabilizes (FG(y) satisfied).

3. Add NoC enforcement benchmarks
Three R2P examples derived from industry Network-on-Chip enforcement specifications (QoS priority bounding, bus lock violation, BIST reconfiguration, fault containment). noc_formulas_4_13 and noc_enforcement_no46 expose the per-implication alive region bug — old code said REALIZABLE, both Strix and the fix say UNREALIZABLE.

4. Strategy verification script (benchmarks/verify_strategies.sh)
For each realizable spec, plays the game with worst-case inputs and checks that FG guarantees stabilize and GF guarantees recur. Catches the reach-phase bug: strategy_bug.sgrk FAIL with AND, PASS with OR.

---

Previous: Fix R2P joint state-dependent alive region

The committed R2P implementation computed alive regions independently per
implication. This is incorrect when multiple R2P implications share output
variables — their alive regions interact through the safety constraint, and
per-implication regions can be non-empty while the joint region is empty.

The fix:

1. Combines all R2P implications into a single demanded predicate:
   demanded(in, out) = ∧_i (¬can_cycle(A_i) ∨ g_i(out))
2. Makes the alive region input-dependent via OutputUnprimedToPrimed
   (primes only output vars, leaves input as identity)
3. Uses output-only quantification throughout the fixpoint
4. Produces a single merged path strategy for all R2P implications

Gives smaller BDDs (n+m free variables instead of 2n+m) and requires
no post-processing to unprime input variables.

---

Summary

• Reorganize benchmarks into R2R, R2P, P2R directories
• Add R2P support: parser, CycleCover, mixed-type rejection
• Fix R2P alive region: joint state-dependent computation
• Fix R2P strategy: AND → OR in path strategy realizable region
• Refactor: shared ComputeR2PAliveRegion method
• Add P2R support: parser, CycleCover
• Benchmarks: stabilize_lock, forced_oscillation, alive_region_pruning, cleaning_robots, power_grid, noc_enforcement, strategy_bug (R2P); cleaning_robots, responsive_toggle, forced_stability, commitment_conflict (P2R)
• Strix comparison: full infrastructure with caching, LaTeX/SVG tables
• Strategy verification: verify_strategies.sh for play-based regression testing

Test plan

• R2P: 40 passed, 0 failed (including noc_enforcement unrealizable + strategy_bug realizable)
• R2R/P2R: all pass
• Mixed type specs correctly rejected
• R2P Strix comparison: sgrk matches Strix on all examples
• noc_formulas_4_13: old code REALIZABLE (wrong), fix UNREALIZABLE (matches Strix)
• strategy_bug: old code strategy stuck at idle, fix reaches alive by step 2
• verify_strategies.sh: strategy_bug PASS after fix, FAIL with old AND

🤖 Generated with Claude Code