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 in predicates.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 repo
• docs/architecture.md — how the layers compose
• code/CLAUDE.md — code architecture, conventions, validity range
• code/README.md — usage and dependencies
• reachability/README.md — reach scope, soundness status
• reachability/WALKTHROUGH.md — standalone analysis writeup
• journal/README.md — journal format conventions
• journal/journal.tex — the journal itself, dated entries
• thesis/CLAUDE.md — the thesis project structure
• fret-pipeline/README.md — FRET naming conventions and pipeline details