dc4cfed61a
Per Dane's question: does LQR actually factor into the 2364x barrier
on n_high_trip, or is that just open-loop plant?
Answer: LQR IS included (A_cl = A - B*K), and the open-loop version is
catastrophically worse. Results on inv2_holds halfspaces:
open-loop LQR closed-loop
fuel_centerline 26.9M K bound 1137 K bound
t_avg_high_trip 788220 K bound 33.2 K bound
n_high_trip 27.4M x bound 1242 x bound
cold_leg_subcooled 1.8M K bound 77.8 K bound
gamma (level) 1.04e13 1.85e4
LQR improves every bound by ~20,000x — dramatic help — but the bounds
are still physically meaningless. The ceiling is set by plant anisotropy
(Lambda=1e-4 vs thermal timescales ~ seconds) forcing P to be
ill-conditioned regardless of LQR tuning. mu (slowest V-decay rate)
barely moves between OL and CL because both share the same slowest
thermal mode.
Clean motivation for the thesis chapter's move to polytopic / SOS
barriers: quadratic Lyapunov hits an anisotropy ceiling that no amount
of controller work can fix.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
pwr-hybrid-3-demo
Preliminary example for the HAHACS thesis — a verified hybrid controller for a small modular PWR startup. Composes three layers into one demonstrable pipeline:
- Discrete layer (
fret-pipeline/): FRET natural-language requirements → LTL → synthesized AIGER controller → state-machine diagram. - Continuous layer (
plant-model/): 10-state point kinetic equation + thermal-hydraulics PWR model with bounded steam-generator heat removal as the disturbance input. - Research context (
thesis/): the HAHACS PhD proposal that motivates and formalizes the methodology.
Layout
pwr-hybrid-3-demo/
CLAUDE.md AI-facing context and architecture map
docs/
architecture.md How the discrete and continuous layers compose
figures/ Shared figures for thesis + talks
fret-pipeline/ FRET → ltlsynt → AIGER → state machine
plant-model/ PWR point kinetics + thermal-hydraulics
reachability/ Continuous-mode verification (linear-model tube + Lyapunov barrier attempt; see README)
julia-port/ Parallel plant-model port + ReachabilityAnalysis.jl scaffold
hardware/ Ovation HIL artifacts (TBD)
claude_memory/ Session notes by AI agents (distilled up into CLAUDE.md over time)
thesis/ [submodule] PhD proposal
presentations/
2026DICE/ [submodule] DICE 2026 abstract
Quickstart
Clone with submodules:
git clone --recurse-submodules <url>
cd pwr-hybrid-3-demo
Run the controller synthesis pipeline:
cd fret-pipeline
python3 scripts/fret_to_synth.py pwr_hybrid_3.json specs/synthesis_config_v3.json
bash scripts/synthesize.sh specs/synthesis_config_v3.json circuits
python3 scripts/trace_aiger.py circuits/PWR_HYBRID_3_DRC.aag diagrams
dot -Tpng diagrams/PWR_HYBRID_3_DRC_states.dot -o diagrams/PWR_HYBRID_3_DRC_states.png
Run the plant model (MATLAB in plant-model/ — Octave compatibility not tested since the LQR pieces landed):
main % original single-scenario demo (null vs operation)
main_mode_sweep % all five DRC modes back-to-back, writes to ../docs/figures/
test_linearize % Jacobian sanity check, saves linearization for reach
Run the reach artifacts (reachability/):
reach_operation % linear reach tube for operation-mode LQR
barrier_lyapunov % Lyapunov-ellipsoid barrier cert attempt (sweeps weights)
Soundness note: the current reach tube is the LINEAR model's tube;
it is not yet a sound over-approximation of the nonlinear plant. See
reachability/README.md § Soundness status.
Prerequisites
- Python 3.10+
- Spot for
ltlsynt(brew install spot) - Graphviz for
dot(brew install graphviz) - MATLAB or GNU Octave for the plant model
- LaTeX (via
latexmk) for the thesis submodule
Further reading
CLAUDE.md— orientation for AI agents working in this repodocs/architecture.md— how the layers composethesis/CLAUDE.md— the thesis project structurefret-pipeline/README.md— FRET naming conventions and pipeline detailsplant-model/README.md— scenario setup and model equations