# Reachability

Continuous-mode verification for the PWR_HYBRID_3 hybrid controller.

## Status

**Per-mode only.** Following the compositionality argument in the thesis:
verify each continuous mode separately, let the DRC handle discrete
switching. Current focus: **operation mode** under LQR feedback.

## What's here

- `linearization_at_op.mat` — A, B, B_w and reference point, generated by
  `../plant-model/test_linearize.m`.
- `reach_linear.m` — box-zonotope propagation of the closed-loop linear
  model under bounded disturbance. Pure MATLAB, no external toolbox.
- `barrier_lyapunov.m` — Lyapunov-ellipsoid barrier certificate for the
  closed-loop linear system. Solves a Lyapunov equation, reports the
  smallest sub-level set containing the initial set and closed under
  the disturbance.
- `reach_operation.m` — end-to-end operation-mode reach: linearize at
  x_op, compute LQR gain, propagate zonotope reach set, check against
  the `t_avg_in_range` predicate.
- `figures/` — generated plots.

## Running

From MATLAB:

```matlab
cd reachability
reach_operation     % computes reach set + plots
barrier_lyapunov    % solves Lyapunov, reports invariant ellipsoid
```

## Tool choice

Currently using a hand-rolled zonotope reach because:
- Avoids a ~0.5 GB CORA install for a first-pass result.
- Linear reach with bounded disturbance has a clean analytic form
  (matrix exponential on the state, integral of e^(A(t-s))·B_w·w ds
  for the disturbance).
- Stays inside MATLAB, which is where the plant model lives.

If we need nonlinear reach (and we will, for non-LQR controllers or
larger reach sets where linearization error matters), the planned
options are CORA (MATLAB) or JuliaReach (port the plant to Julia).

## What this does NOT do yet

- Nonlinear reach for the original P controller on operation.
- Heatup reach (the ramped reference makes x* time-varying — needs
  trajectory-LQR or a different formulation).
- Shutdown, scram, initialization reach.
- Hybrid-system level verification (mode switching validity).