cebf8c167a
Folds three previously-separate pieces into one preliminary-example repo for the HAHACS thesis: - thesis/ (submodule) → gitea Thesis.git — the PhD proposal - fret-pipeline/ — FRET requirements to AIGER controller (was ~/Documents/fret_processing/; prior single-commit history abandoned per user decision) - plant-model/ — 10-state PKE + lumped T/H PWR model (was ~/Documents/PKE_Playground/; never version-controlled before) - presentations/2026DICE/ (submodule) → gitea 2026DICE.git - reachability/, hardware/ — empty placeholders for Thrust 3 and HIL - docs/architecture.md — how the discrete and continuous layers compose - claude_memory/ — session notes and scratch knowledge pattern Plant model refactored to thesis naming (x, plant, u, ref); pke_th_rhs now takes u as an explicit arg instead of reading rho_ext from the params struct. First two controllers built to the contract u = ctrl_<mode>(t, x, plant, ref): ctrl_null (baseline) and ctrl_operation (stabilizing, proportional on T_avg). Validated under a 100% -> 80% Q_sg step: ctrl_operation reduces steady-state T_avg drift ~47% vs. the unforced plant. Root CLAUDE.md emphasizes that CLAUDE.md files are living documents and that any knowledge not captured before a session ends is lost forever; claude_memory/ holds the session-level notes that haven't stabilized enough to graduate into a CLAUDE.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
95 lines
4.2 KiB
Markdown
95 lines
4.2 KiB
Markdown
# Architecture — how the layers compose
|
|
|
|
This is the integration guide. Each subdirectory has its own docs for internal
|
|
detail; this file explains the interfaces between them.
|
|
|
|
## The three layers of a hybrid controller
|
|
|
|
The HAHACS methodology (see `thesis/3-research-approach/approach.tex`) splits
|
|
verification into two decoupled problems:
|
|
|
|
1. **Discrete layer** — proves that mode switching is correct given guard
|
|
predicates on the continuous state. Handled by reactive synthesis of an
|
|
AIGER circuit from LTL specifications. Lives in `fret-pipeline/`.
|
|
2. **Continuous layer** — proves that each continuous controller (one per
|
|
discrete mode) satisfies its entry/exit/safety obligations. Handled by
|
|
reachability analysis (transitory modes) or barrier certificates
|
|
(stabilizing modes). Lives in `plant-model/` (dynamics) and `reachability/`
|
|
(verification, TBD).
|
|
|
|
The interface between them is a small set of predicates over the continuous
|
|
state: the guards `G` that transition between modes, and the invariants `Inv`
|
|
that the continuous mode must maintain.
|
|
|
|
## Interface: predicates bridging discrete and continuous
|
|
|
|
FRET variables of the form `control_<group> = q_<value>` define the discrete
|
|
state space. Everything else in the FRET export is treated as a boolean
|
|
environment input. Real plant quantities are continuous, so the boolean
|
|
environment inputs are *abstractions* of continuous predicates.
|
|
|
|
For the PWR_HYBRID_3 example, representative predicates:
|
|
|
|
| FRET input | Continuous predicate | Plant-model source |
|
|
|---|---|---|
|
|
| `t_avg_above_min` | `T_avg > T_min` (where `T_avg = T_c`) | `pke_th_rhs.m` state `T_c` |
|
|
| `t_max_exceeded` | `T_hot > T_max` (where `T_hot = 2*T_c - T_cold`) | algebraic output |
|
|
| `inv1_holds` | domain-specific safety invariant | combine from states |
|
|
| `manual_reset` | operator input | exogenous |
|
|
|
|
The continuous controller is responsible for driving `T_avg`, `T_hot`, `n`, etc.
|
|
so the predicates hold (or don't hold) at the right times. The discrete
|
|
controller is responsible for choosing the correct mode given the predicate
|
|
truth values.
|
|
|
|
## Data flow
|
|
|
|
```
|
|
Written procedure
|
|
|
|
|
v (manual encoding in FRET GUI)
|
|
FRET JSON export <---- fret-pipeline/pwr_hybrid_3.json
|
|
|
|
|
v (fret_to_synth.py)
|
|
Synthesis config JSON <---- fret-pipeline/specs/synthesis_config_v3.json
|
|
| (LTL + mode groups + mutex constraints + inputs/outputs)
|
|
|
|
|
v (synthesize.sh -> ltlsynt)
|
|
AIGER circuit <---- fret-pipeline/circuits/*.aag
|
|
|
|
|
v (trace_aiger.py)
|
|
State machine DOT/SVG/PNG <---- fret-pipeline/diagrams/*
|
|
|
|
|
v (eyeball / future automation)
|
|
Stateflow model <---- TBD; known pain point in workflow
|
|
|
|
Continuous side, in parallel:
|
|
plant-model/main.m defines Q_sg(t)
|
|
plant-model/pke_solver.m runs ode15s
|
|
plant-model/plot_pke_results.m visualizes
|
|
reachability/ (empty) will verify each
|
|
continuous mode against the guards from
|
|
synthesis_config_v3.json
|
|
```
|
|
|
|
## Current integration state
|
|
|
|
- Discrete synthesis: **works end-to-end.** `pwr_hybrid_3.json` synthesizes
|
|
to `PWR_HYBRID_3_DRC.aag` and traces to a state-machine diagram.
|
|
- Continuous simulation: **works end-to-end.** The PKE model runs
|
|
load-following transients driven by `Q_sg(t)`.
|
|
- Cross-layer check: **not yet wired.** Nothing currently proves that the
|
|
continuous dynamics in `plant-model/` satisfies the guards assumed by
|
|
`fret-pipeline/`. That is the next piece (`reachability/`).
|
|
- Thesis integration: **loose.** Thesis currently uses a hand-drawn TikZ
|
|
figure for the reactor automaton. Once the pipeline output stabilizes,
|
|
swap it for an `\includegraphics` of the generated `.png` from
|
|
`docs/figures/`.
|
|
|
|
## Open questions tracked elsewhere
|
|
|
|
The thesis CLAUDE.md enumerates open technical questions (numerical barriers,
|
|
timing verification, partial observability). When those get resolved in the
|
|
proposal, the implementation lands in this repo — usually as a new
|
|
subdirectory or as additions to an existing one.
|