# 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:

```bash
git clone --recurse-submodules <url>
cd pwr-hybrid-3-demo
```

Run the controller synthesis pipeline:

```bash
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:

```bash
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:

```bash
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](https://spot.lre.epita.fr/) for `ltlsynt` (`brew install spot`).
- [Graphviz](https://graphviz.org/) 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