8d2c7d0956
Morning-review point 3 result: tight-entry heatup PJ reach with
Q_sg in [0, 5% P0] as a bounded parameter (augmented state x[10]).
T=60s: 7042 sets in 394s — T_c in [270.97, 291.0] — low-trip × loose
T=300s: 100k sets budget exhausted in 5400s —
T_c in [219.4, 316.3] — low-trip × loose
Compared to the no-disturbance tight-entry run (all 6 halfspaces at
300s, T_c in [281.05, 291.0]), the bounded steam-dump disturbance
costs the low-T_avg-trip discharge even at 60s. Physically correct
— steam dump pulls heat through secondary, cascades into cold-leg
and T_avg. The reach tube accurately captures this coupling.
Thesis-relevant finding: without modeled disturbance bounds, reach
tubes are over-optimistic. Quantifies how much of the prior
"all 6 halfspaces" result came from Q_sg=0 simplification vs.
actual controller robustness.
Results saved to results/reach_heatup_pj_with_steam_dump.mat.
Journal entry updated with the per-horizon table + decision box on
what this means for thesis claims.
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 (
code/): 10-state point kinetic equation + thermal-hydraulics PWR model with bounded steam-generator heat removal as the disturbance input. Controllers, linearization, LQR, reach-tube propagator, Lyapunov barrier — all Julia. - Verification artifacts (
reachability/): predicate concretizations (single source of truth inpredicates.json) and the standalone reach analysis writeup (WALKTHROUGH.md). - Research context (
thesis/): the HAHACS PhD proposal. - Lab journal (
journal/): chronological invention log in LaTeX. - Predicate explorer app (
app/): Pluto.jl notebook bridging FRET predicates and continuous-state halfspaces.
Layout
pwr-hybrid-3-demo/
CLAUDE.md AI-facing context and architecture map
docs/
architecture.md How the layers compose
figures/ Shared figures for thesis + talks
fret-pipeline/ FRET → ltlsynt → AIGER → state machine
code/ Plant model, controllers, reach (all Julia)
reachability/ predicates.json + WALKTHROUGH.md
app/ Pluto.jl predicate explorer
journal/ LaTeX lab notebook
hardware/ Ovation HIL artifacts (TBD)
claude_memory/ Short AI-context notes
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 and reach analysis:
cd code
julia --project=. -e 'using Pkg; Pkg.instantiate()' # first time only
julia --project=. scripts/main_mode_sweep.jl # all 5 DRC modes
julia --project=. scripts/reach_operation.jl # operation-mode linear reach
julia --project=. scripts/barrier_lyapunov.jl # Lyapunov barrier
julia --project=. scripts/barrier_compare_OL_CL.jl # OL vs CL barrier
julia --project=. scripts/reach_heatup_nonlinear.jl # nonlinear heatup (10s cap)
Open the predicate explorer:
cd app
julia --project=. -e 'using Pluto; Pluto.run()'
# Browser opens; navigate to predicate_explorer.jl
Soundness note: the current reach tubes are over-approximations
of the LINEAR model, not sound over-approximations of the nonlinear
plant. See reachability/README.md and reachability/WALKTHROUGH.md.
Prerequisites
- Julia 1.10+ (via
juliaup). - Python 3.10+ (FRET pipeline only).
- Spot for
ltlsynt(brew install spot). - Graphviz for
dot(brew install graphviz). - LaTeX (via
latexmk) for the thesis + journal builds.
Further reading
CLAUDE.md— orientation for AI agents working in this repodocs/architecture.md— how the layers composecode/CLAUDE.md— code architecture, conventions, validity rangecode/README.md— usage and dependenciesreachability/README.md— reach scope, soundness statusreachability/WALKTHROUGH.md— standalone analysis writeupjournal/README.md— journal format conventionsjournal/journal.tex— the journal itself, dated entriesthesis/CLAUDE.md— the thesis project structurefret-pipeline/README.md— FRET naming conventions and pipeline details