# Reachability

Continuous-mode verification for the PWR_HYBRID_3 hybrid controller.

## Soundness status: APPROXIMATE

The current linear-reach results are **not a sound reach tube for
the physical plant**. They are sound over-approximations of the
*linearized* closed-loop system ($A_{\mathrm{cl}} = A - BK$ around
$x_{\mathrm{op}}$) under bounded disturbance. The linear model is
itself an approximation of the nonlinear plant (`../code/src/pke_th_rhs.jl`),
and that approximation error is not currently bounded or inflated
into the tube.

Two paths to upgrade to a sound result:

1. **Nonlinear reach directly** — TMJets (Taylor-model integration)
   via ReachabilityAnalysis.jl. Currently limited to ~10-second
   horizons by prompt-neutron stiffness; needs a reduced-order PKE
   (prompt-jump approximation) to extend to mode-obligation horizons.
2. **Linear reach + Taylor-remainder inflation** — compute an upper
   bound on `||f_nl(x, u) - (A x + B u)||` over the reach set and
   inflate the linear tube by that bound. Cheaper, still rigorous.

Both are thesis-blocking for any safety claim. The current
5-orders-of-margin buffer (reach envelope ~0.03 K against a
5 K safety band on $T_c$) means linearization error would have to
be huge to invalidate the conclusion — but that's vibes, not a proof.

## Related open issues

- **Saturation semantics.** `ctrl_heatup.jl` uses `clamp(u, u_min, u_max)`.
  Saturation is formally a 3-mode piecewise-affine system. For
  heatup reach this must be handled as (a) hybrid locations, or
  (b) proven dormant via reach on `u_unsat`. Not modeled in the
  current artifacts (operation-mode LQR saturation is dormant in
  practice but the proof is implicit).
- **Parametric uncertainty in α_f, α_c.** Real plants have α drift
  with burnup (~20%), boron (α_c ranges 10×), xenon. The
  feedback-linearization in `ctrl_heatup` assumes exact α; a robust
  treatment would make α an interval and propagate parametric reach.
  Currently idealized.

## What's here

**Per-mode only.** Following the compositionality argument in the
thesis: verify each continuous mode separately, let the DRC handle
discrete switching.

Files:

- `predicates.json` — single source of truth for predicate
  concretizations. Three groups:
  - `operational_deadbands` — soft bands used by DRC for mode
    transitions (`t_avg_above_min`, `t_avg_in_range`, `p_above_crit`).
  - `safety_limits` — hard one-sided halfspaces (fuel centerline,
    trip setpoints, subcooling, heatup-rate bounds).
  - `mode_invariants` — `inv1_holds`, `inv2_holds` as conjunctions
    of safety limits.
  - `mode_boundaries` — per-mode $X_{\mathrm{entry}}$, $X_{\mathrm{safe}}$,
    $X_{\mathrm{exit}}$, $T_{\min}$, $T_{\max}$.

- `WALKTHROUGH.md` — standalone document explaining the reach-obligation
  taxonomy, per-mode entry/exit definitions, current results, soundness
  status. Read this for the full story.

The reach code itself lives in `../code/`:

- `../code/src/reach_linear.jl` — hand-rolled box reach propagator.
- `../code/src/load_predicates.jl` — reads `predicates.json`.
- `../code/scripts/reach_operation.jl` — operation-mode linear reach.
- `../code/scripts/barrier_lyapunov.jl` — Lyapunov barrier attempt.
- `../code/scripts/barrier_compare_OL_CL.jl` — OL vs CL comparison.
- `../code/scripts/reach_heatup_nonlinear.jl` — TMJets nonlinear reach
  (heatup, saturation-disabled, 10-second horizon cap).

## Running

```bash
cd code
julia --project=. scripts/reach_operation.jl
julia --project=. scripts/barrier_lyapunov.jl
julia --project=. scripts/barrier_compare_OL_CL.jl
julia --project=. scripts/reach_heatup_nonlinear.jl
```

Results save here as `*.mat` (gitignored).

## What this does NOT do yet

- Any sound reach tube (see top of this file).
- Nonlinear reach on horizons > 10 s (needs reduced-order PKE).
- Shutdown, scram, initialization reach.
- Hybrid-system level verification (mode switching validity).
- Parametric robustness to α_f, α_c drift.
- Polytopic or SOS barriers — the canonical quadratic Lyapunov
  barrier fails structurally on this plant (see `WALKTHROUGH.md`
  and the OL-vs-CL comparison script).