Dane Sabo cebf8c167a Initial umbrella repo: thesis + FRET pipeline + plant model with first controllers

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>

2026-04-16 16:24:11 -04:00

4.2 KiB

Raw Blame History

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:

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/.
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.

4.2 KiB Raw Blame History