PWR-HYBRID-3/CLAUDE.md

CLAUDE.md

Guidance for Claude Code (and any AI agent) working in this repository.

Living documentation — update these files

CLAUDE.md files are living. This one and the ones in subdirectories. When you learn something new about the system that a future agent would benefit from, update the appropriate CLAUDE.md before the session ends. Context that exits a session uncaptured is lost forever — treat this as the single most important rule in this repo.

Where to write:

• Stable, authoritative knowledge (architecture, conventions, interfaces, design decisions) → the relevant CLAUDE.md. Root for cross-cutting; subdirectory for layer-specific.
• Session-level findings, in-progress investigations, paths that didn't pan out → claude_memory/YYYY-MM-DD-topic.md. See claude_memory/README.md for the pattern.

When to write:

• After a non-trivial debugging session (what broke, root cause, how you knew).
• After an architectural or structural decision (what we chose, what we rejected, why).
• After discovering a non-obvious fact (subtle constraint, undocumented tool behavior, counterintuitive data format).
• Before ending a session where you explored paths that didn't pan out — so the next agent doesn't waste effort redoing them.

Over time, session notes that stabilize get distilled up into the relevant CLAUDE.md; the rest get archived or deleted. This is a discipline, not automation — do the graduation explicitly when knowledge becomes authoritative.

What this is

The preliminary example for the HAHACS thesis — a PWR startup controller demonstrating the full pipeline from written operating procedures to verified hybrid controller. This repo composes three layers of the same story:

Layer	Location	Role	Thesis mapping
Story	thesis/ (submodule)	The PhD proposal: math, prose, claims	Motivates and defines the methodology
Discrete	fret-pipeline/	FRET requirements → LTL → ltlsynt → AIGER circuit → state machine	Implements Thrust 1 + 2
Continuous + Verification	code/ + reachability/	10-state PKE + thermal-hydraulics PWR model, controllers, reach machinery (all Julia) plus predicates.json and WALKTHROUGH.md	Plant + Thrust 3 (reachability / barrier certs)
Journal	journal/	LaTeX invention log, dated entries	Project history / re-derivability
App	app/	Pluto.jl predicate explorer	FRET-adjacent UI for hybrid-systems groups
Hardware	hardware/	Ovation HIL artifacts	Integration milestone — currently empty
Deliverables	presentations/	Conference papers and talks (submodules)	Dissemination

Running example: the PWR_HYBRID_3 controller. The discrete automaton it synthesizes is literally the state machine drawn in thesis/3-research-approach/approach.tex Figure 1 (Cold Shutdown → Heatup → Power Operation, with SCRAM).

How changes flow

1. Requirement change. Edit the FRET export (fret-pipeline/pwr_hybrid_3.json) → run fret-pipeline/scripts/fret_to_synth.py → re-synthesize via synthesize.sh → re-trace via trace_aiger.py. New .svg / .dot / .png land in fret-pipeline/diagrams/. Copy the figure you want to cite into docs/figures/ so the thesis can pick it up.
2. Plant change. Edit code/src/pke_params.jl or dynamics in code/src/pke_th_rhs.jl → re-run code/scripts/main_mode_sweep.jl to verify behavior. Steady-state values feed the T_avg, P_crit thresholds via reachability/predicates.json — if you change parameters here, the predicate concretization may need to follow.
3. Verification work. Continuous-mode verification reads the FRET-side predicates from reachability/predicates.json and the dynamics from code/src/pke_th_rhs.jl. Reach scripts in code/scripts/reach_*.jl and barrier_*.jl. Results land back in reachability/*.mat (gitignored).
4. Thesis edit. cd thesis && <edit> && git commit && git push origin main, then from the umbrella root: git add thesis && git commit to bump the submodule pointer.

Where to look for what

• Reactor physics, steady-state, ODE dynamics, controllers, reach, barrier → code/
• Predicate concretizations (the seam between FRET and reach) → reachability/predicates.json
• Reach analysis writeup → reachability/WALKTHROUGH.md
• Controller synthesis, requirements, state machines → fret-pipeline/
• Research narrative, math, claims, citations → thesis/
• Shared figures (for the thesis or talks) → docs/figures/
• How the layers compose → docs/architecture.md
• Project history / invention log → journal/
• Predicate-explorer GUI → app/

Submodule rituals

• Fresh clone: git clone <url> && git submodule update --init --recursive (or git clone --recurse-submodules <url>). Without this, thesis/ and presentations/2026DICE/ are empty directories.
• Editing the thesis: cd thesis && git checkout main first — submodules default to detached HEAD. Then edit, commit, push inside the submodule, then cd .. and commit the new submodule pointer in the umbrella.
• Pulling upstream thesis changes: cd thesis && git pull origin main, then commit the new pointer in the umbrella.

Conventions

• FRET variables: control_<group> = q_<value> for modes; everything else is an environment input. See fret-pipeline/README.md for the full naming rule.
• Plant model units: internal SI (W, kg, °C); printed/plotted in °F.
• Continuous state vector: x = [n; C1..C6; T_f; T_c; T_cold]. Guards in FRET should reference the algebraic outputs (T_hot, T_avg) or direct states, not derived quantities.
• Q_sg(t) is the bounded disturbance — never treat T_cold as an input.
• The continuous toolchain is Julia. The earlier MATLAB implementation was ported on 2026-04-20 and deleted; recover via git history if archaeologically needed.

What's deliberately missing (so you don't go looking)

• LTL-to-Stateflow translator — there's a known pain point in the thesis workflow where AIGER circuits still need to become Stateflow. Not yet automated. Current path: generate AIGER → eyeball the state machine diagram → hand-translate to Stateflow. Roadmapped.
• Hardware bring-up (Ovation DCS) — scheduled for the integration thrust. hardware/ is a placeholder.
• Continuous-mode verification — partial. Linear reach for operation mode discharges all 6 inv2_holds halfspaces (approximate, not sound). Lyapunov-ellipsoid barrier fails structurally (anisotropy ceiling — see reachability/WALKTHROUGH.md). Nonlinear reach (TMJets) functional to 10 s; needs reduced-order PKE for hours-long horizons.
• Polytopic / SOS barriers — flagged in WALKTHROUGH as the next-step alternative to the failing quadratic Lyapunov barrier.
• Reduced-order (prompt-jump) PKE — known remedy for nonlinear reach stiffness, not yet implemented.