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