Multi-session work bundle on a draft branch. Splits into a clean
sequence of commits later; pushed here so it isn't lost on a reboot.
Reach work
- code/scripts/reach/reach_scram_pj.jl: shutdown_margin halfspace
X_exit (replaces "n <= 1e-4 AND T_f bound" framing); per-step
envelope extraction added.
- code/scripts/reach/reach_scram_pj_fat.jl: per-step envelope
extraction added; shutdown_margin discharge logic mirrored from the
tight scram script. 3 probes (10/30/60s) all discharge from the
fat union polytope.
- code/scripts/reach/reach_scram_full_fat.jl (NEW): full nonlinear
PKE scram reach with fat entry. Hits the stiffness wall at
~1.5 s plant time as expected; saves NaN-tolerant per-step
envelopes. Demonstrates concretely why PJ is the right tool for
the longer-horizon proof.
- code/scripts/reach/reach_heatup_pj.jl: T_REF_START_C constant
(entry-conditioned ramp) replaces T_STANDBY-init that was making
the FL controller command cooling at t=0. Per-step extraction
already in place.
- code/configs/heatup/tight.toml: bumped maxsteps; probe horizon
parameterized.
Hot-standby SOS barrier
- code/scripts/barrier/barrier_sos_2d_shutdown.jl (NEW): mirrors the
operation SOS machinery on the hot-standby thermal projection.
Includes the eps-slack pattern (so feasibility doesn't silently
collapse to B == 0).
- code/scripts/barrier/barrier_sos_2d.jl: refactored to use the same
helper.
- code/src/sos_barrier.jl (NEW): solve_sos_barrier_2d helper module
factoring out the SOS construction; eps-slack with eps_cap=1.0 to
avoid unbounded primal.
Library
- code/src/pke_states.jl (NEW): single source of truth for canonical
initial-condition vectors per DRC mode (op, shutdown, heatup) keyed
off plant + predicates.
- code/scripts/sim/{main_mode_sweep,validate_pj}.jl, code/CLAUDE.md:
migrated to pke_states.
Predicates + invariants
- reachability/predicates.json: new shutdown_margin predicate (1%
dk/k tech-spec floor, expressed as alpha_f*T_f + alpha_c*T_c
halfspace). Used as scram X_exit.
Plot script
- code/scripts/plot/plot_reach_tubes.jl: plot_tubes_scram_pj() with
variant=:fat|:tight knob; plot_tubes_scram_full() for full-PKE
3-panel (T_c, T_f, rho); plot_tubes_heatup_pj() reads results/
not reachability/.
Journal + memory
- journal/entries/2026-04-27-shutdown-sos-and-scram-X_exit.tex (NEW):
long-form entry on the SOS hot-standby barrier and the scram X_exit
refactor.
- journal/journal.tex: input chain updated.
- claude_memory/ — three new session notes:
* 2026-04-27-scram-X_exit-shutdown-margin.md
* 2026-04-28-DICE-2026-conference-intel.md (people, sessions,
strategic notes for the May 12 talk)
* 2026-04-28-path1-sos-pj-sketch.md (sketch of nonlinear-SOS via
polynomial multiply-through; saved for an overnight session)
Docs
- docs/model_cheatsheet.md (NEW): one-page reference of state vector,
dynamics, constants, modes, predicates, sanity numbers — the talk
prep cheatsheet Dane asked for.
- docs/figures/reach_*_tubes.png: regenerated with the new mat data.
- presentations/prelim-presentation/outline.md: revised arc per the
April-28 review pass (cuts: Lyapunov-fails standalone slide,
operation-tube standalone slide, SOS standalone; adds: scopes-of-
control framing, scram on the headline result slide).
- app/predicate_explorer.jl: minor.
Hacker-Split: end-of-session scratch bundle
198 lines
8.8 KiB
Markdown
198 lines
8.8 KiB
Markdown
# CLAUDE.md
|
||
|
||
Guidance for Claude Code (and any AI agent) working in this subdirectory.
|
||
|
||
See also: the parent repo's `CLAUDE.md` (living-documentation rule —
|
||
update this file when new knowledge is created), `claude_memory/` for
|
||
session notes, and `../journal/` for the long-form invention log.
|
||
|
||
## What this is
|
||
|
||
The full plant-model + reachability toolchain for the PWR_HYBRID_3
|
||
preliminary example. All Julia — the earlier MATLAB implementation
|
||
was ported end-to-end on 2026-04-20 and deleted. A 10-state point
|
||
kinetic equation (PKE) model of a PWR coupled with lumped-parameter
|
||
thermal-hydraulics, plus mode-specific continuous controllers, linear
|
||
reach-set machinery, Lyapunov-barrier attempt, and scaffolding for
|
||
nonlinear reach via TMJets.
|
||
|
||
The model is being developed for hybrid-systems reachability analysis.
|
||
The end goal is nonlinear reach (sound, not linearized) over per-mode
|
||
reach-avoid obligations, which will require a reduced-order PKE to
|
||
eliminate prompt-neutron stiffness.
|
||
|
||
## Naming convention (thesis-aligned)
|
||
|
||
Continuous state and control-theory notation matches the thesis:
|
||
|
||
| Symbol | Meaning |
|
||
|---|---|
|
||
| `t` | time [s] |
|
||
| `x` | continuous state vector, `[n; C1..C6; T_f; T_c; T_cold]` |
|
||
| `plant` | parameter NamedTuple from `pke_params()` |
|
||
| `u` | control input: external rod reactivity [dk/k] |
|
||
| `Q_sg` | bounded disturbance: SG heat removal [W], as a callable `Q_sg(t)` |
|
||
| `ref` | reference/setpoint NamedTuple (e.g. `ref.T_avg`) |
|
||
|
||
`T_avg = T_c` (algebraic alias); `T_hot = 2*T_c - T_cold` (linear
|
||
coolant profile assumption).
|
||
|
||
## Running
|
||
|
||
From the project root:
|
||
|
||
```bash
|
||
cd code
|
||
julia --project=. -e 'using Pkg; Pkg.instantiate()' # first time only
|
||
|
||
julia --project=. scripts/main_mode_sweep.jl # runs all 5 DRC modes
|
||
julia --project=. scripts/reach_operation.jl # operation-mode linear reach
|
||
julia --project=. scripts/barrier_lyapunov.jl # Lyapunov-ellipsoid barrier
|
||
julia --project=. scripts/barrier_compare_OL_CL.jl # OL vs CL barrier bounds
|
||
julia --project=. scripts/reach_heatup_nonlinear.jl # nonlinear heatup reach (10s max, stiffness-limited)
|
||
julia --project=. scripts/sim_sanity.jl # operation-mode nominal sim
|
||
julia --project=. scripts/sim_heatup.jl # heatup nominal sim
|
||
```
|
||
|
||
Figures save to `../docs/figures/`. Reach results save to
|
||
`../reachability/*.mat` (gitignored).
|
||
|
||
## Architecture
|
||
|
||
```
|
||
code/
|
||
Project.toml Julia package manifest
|
||
README.md usage overview
|
||
src/
|
||
pke_params.jl plant parameters and derived steady state
|
||
pke_states.jl canonical ICs for every DRC mode (single source)
|
||
pke_th_rhs.jl dynamics f(t, x, plant, Q_sg, u)
|
||
pke_linearize.jl numerical (A, B, B_w) Jacobians
|
||
pke_solver.jl closed-loop OrdinaryDiffEq driver
|
||
plot_pke_results.jl 4-panel results plot (Plots.jl)
|
||
reach_linear.jl hand-rolled box reach propagator
|
||
load_predicates.jl reads reachability/predicates.json
|
||
sos_barrier.jl solve_sos_barrier_2d helper (SOS feasibility +
|
||
ε-slack pattern; used by barrier_sos_2d{,_shutdown}.jl)
|
||
controllers/
|
||
controllers.jl ctrl_null, shutdown, heatup, operation,
|
||
operation_lqr factory, scram
|
||
ctrl_heatup_unsat.jl saturation-disabled variant for reach
|
||
scripts/
|
||
main_mode_sweep.jl runs every mode, saves all figures
|
||
sim_sanity.jl operation-mode Rodas5 sim (MATLAB-parity check)
|
||
sim_heatup.jl heatup Rodas5 sim
|
||
reach_operation.jl linear reach tube + inv2_holds check
|
||
barrier_lyapunov.jl Lyapunov barrier sweep
|
||
barrier_compare_OL_CL.jl OL vs CL barrier comparison
|
||
reach_heatup_nonlinear.jl TMJets nonlinear reach (10s horizon cap)
|
||
```
|
||
|
||
## Controller contract
|
||
|
||
```julia
|
||
u = ctrl_mode(t, x, plant, ref) # all five args required
|
||
```
|
||
|
||
Pure function. Returns scalar `u` (external rod reactivity in `dk/k`).
|
||
All four signature args are required even if unused — lets the solver
|
||
swap controllers by function reference without caring which one it is.
|
||
|
||
## Solver contract
|
||
|
||
```julia
|
||
t, X, U = pke_solver(plant, Q_sg, ctrl_fn, ref, tspan; x0=nothing, verbose=true)
|
||
```
|
||
|
||
Returns `(t::Vector, X::Matrix, U::Vector)` where `X[k, :]` is the
|
||
state at time `t[k]` and columns of X match the state vector ordering.
|
||
The underlying integrator is `Rodas5` from OrdinaryDiffEq (stiff-aware,
|
||
matches the MATLAB `ode15s` behavior we validated against). Optional
|
||
`x0` argument for starting from a non-equilibrium IC (heatup, shutdown).
|
||
|
||
## Key design decisions
|
||
|
||
- **`Q_sg` is the disturbance, never an actuator.** Cold leg
|
||
temperature is a dynamic state resulting from SG heat removal — the
|
||
reachability formulation needs `Q_sg ∈ [Q_min, Q_max]` as a bounded
|
||
disturbance, not a control input.
|
||
- **`u` is explicit.** `pke_th_rhs!` takes `u` directly instead of
|
||
reading it from the plant struct.
|
||
- **Controller gains live in the controller file.** Rough-out phase —
|
||
once we tune more than one mode we'll lift to a config struct.
|
||
- **`Rodas5` is required** because the system is stiff:
|
||
`Lambda` (~10⁻⁴ s) vs thermal time constants (~10–100 s).
|
||
- **LQR gain is cached** in a `Ref` inside `ctrl_operation_lqr_factory`.
|
||
Reconstruct the factory (not just call it) to retune.
|
||
- **Single-point ICs live in `pke_states(plant; predicates=...)`.** Returns
|
||
a NamedTuple with `T_standby`, `op`, `shutdown`, `heatup` — every script
|
||
that needs an IC for forward sim or equilibrium-finding pulls from here.
|
||
X_entry *polytopes* (for reach) live in `predicates.json` and are loaded
|
||
separately by reach scripts; don't conflate the two.
|
||
- **SOS barrier programs need ε-slack + scale cap.** The naive feasibility
|
||
formulation silently returns `B ≡ 0`. `solve_sos_barrier_2d` in
|
||
`src/sos_barrier.jl` bakes in the (ε > 0, capped) pattern. Use it for
|
||
any new SOS barrier work.
|
||
- **Plant parameters live in `pke_params()` as a NamedTuple.** For
|
||
reach analysis (TMJets) we duplicate them as `const` globals in
|
||
each reach script — `@taylorize` needs compile-time constants, not
|
||
struct-field accesses. Keep these in sync.
|
||
|
||
## Conventions
|
||
|
||
- One function per file where natural; group related functions in
|
||
one file when they're small (the controllers all live in one file).
|
||
- Internal model uses SI (W, kg, °C); printed/plotted temperatures
|
||
in °F.
|
||
- Reference setpoints in SI (so `ref.T_avg` is in °C).
|
||
- Controllers are pure functions — no persistent state. If a mode
|
||
needs integral action, augment `x`, don't hide state in globals.
|
||
(Exception: the LQR factory caches K in a closure, but that's
|
||
immutable after construction.)
|
||
|
||
## Model validity range
|
||
|
||
The feedback coefficients `alpha_f`, `alpha_c` are *linear* slopes
|
||
taken about the full-power operating point `(T_f0, T_c0)`. They become
|
||
unphysical when extrapolated far from that reference. True cold
|
||
shutdown (~50 °C everywhere) violates the linear-coefficient
|
||
assumption.
|
||
|
||
**Trust range:** roughly ±50 °C around the operating point.
|
||
"Shutdown" in this demo means hot standby (~275 °C per
|
||
`predicates.json` `T_standby`), not cold shutdown. Extending to
|
||
cold-shutdown semantics requires piecewise-linear or table-lookup
|
||
temperature coefficients — separate modeling project.
|
||
|
||
## For reachability work
|
||
|
||
- `pke_th_rhs!(dx, x, t, plant, Q_sg, u)` is the `ẋ = f(x, u)` with
|
||
`Q_sg` as the disturbance `w`.
|
||
- Use `pke_linearize(plant; x_star, u_star, Q_star)` for `(A, B, B_w)`
|
||
at any operating point.
|
||
- Safe regions come from `../reachability/predicates.json` — three
|
||
layers: `operational_deadbands` (DRC transitions),
|
||
`safety_limits` (hard halfspaces), `mode_invariants` (conjunctions
|
||
used by per-mode reach).
|
||
- Do NOT try to verify the whole hybrid system at once. Pick one
|
||
mode, compute its reach set, discharge the per-mode obligation.
|
||
- Linear reach in `scripts/reach_operation.jl`; nonlinear (TMJets)
|
||
in `scripts/reach_heatup_nonlinear.jl`.
|
||
|
||
## Robustness caveats (idealized in current artifacts)
|
||
|
||
- **α_f, α_c are treated as known exactly.** The feedback-linearization
|
||
in `ctrl_heatup` assumes the controller's α matches the plant's;
|
||
real reactors have α drift (burnup, boron, xenon). Robust treatment
|
||
= α as bounded parametric uncertainty.
|
||
- **Saturation is a hybrid sub-mode.** `ctrl_heatup`'s `clamp(u, ...)`
|
||
is formally piecewise affine. Current reach treats it as dormant
|
||
(true for operation/LQR, near-true for the demo heatup trajectory).
|
||
A rigorous heatup reach has to model saturation regions explicitly.
|
||
- **Linear-model reach is not sound for the nonlinear plant.** The
|
||
linear-reach artifacts produce a sound over-approximation of the
|
||
LINEAR model's reach set, not of the plant's. To upgrade:
|
||
nonlinear reach directly (TMJets, once the reduced-order PKE
|
||
eliminates prompt-neutron stiffness), or Taylor-remainder inflation
|
||
on linear tubes.
|