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>
111 lines
3.6 KiB
Markdown
111 lines
3.6 KiB
Markdown
# FRET-to-Synthesis Pipeline
|
|
|
|
A deterministic pipeline for converting FRET natural-language requirements into
|
|
synthesized reactive controllers, with automatic state machine visualization.
|
|
|
|
```
|
|
pwr_hybrid_3.json FRET export (source of truth)
|
|
|
|
|
v
|
|
scripts/fret_to_synth.py Auto-discover modes, encode as booleans
|
|
|
|
|
v
|
|
specs/synthesis_config_v3.json ltlsynt-ready config
|
|
|
|
|
v
|
|
scripts/synthesize.sh Run ltlsynt (reactive synthesis)
|
|
|
|
|
v
|
|
circuits/*.aag Synthesized controller (AIGER circuit)
|
|
|
|
|
v
|
|
scripts/trace_aiger.py Exhaustive eval, guard extraction, DOT
|
|
|
|
|
v
|
|
diagrams/*_states.dot/png/svg State machine with guard conditions
|
|
```
|
|
|
|
## Quick Start
|
|
|
|
```bash
|
|
# 1. Convert FRET export to synthesis config
|
|
python3 scripts/fret_to_synth.py pwr_hybrid_3.json specs/synthesis_config_v3.json
|
|
|
|
# 2. Synthesize the controller
|
|
bash scripts/synthesize.sh specs/synthesis_config_v3.json circuits
|
|
|
|
# 3. Trace and visualize
|
|
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
|
|
```
|
|
|
|
## Prerequisites
|
|
|
|
- **Python 3.10+** (no external packages required)
|
|
- **[Spot](https://spot.lre.epita.fr/)** for `ltlsynt` (`brew install spot`)
|
|
- **[Graphviz](https://graphviz.org/)** for `dot` (`brew install graphviz`)
|
|
|
|
## FRET Naming Conventions
|
|
|
|
The pipeline auto-discovers mode variables and environment inputs from your FRET
|
|
export. To make this work, follow these naming rules in FRET:
|
|
|
|
### Mode variables: `control_* = q_*`
|
|
|
|
Any variable whose name starts with `control_` is treated as a discrete mode
|
|
variable. Its values must start with `q_`. Examples:
|
|
|
|
```
|
|
control_mode = q_shutdown (a reactor operating mode)
|
|
control_pump = q_running (a pump state)
|
|
control_valve = q_open (a valve position)
|
|
```
|
|
|
|
The script discovers these by regex-scanning the LTL formulas. Multiple control
|
|
groups are supported -- each gets its own set of boolean outputs and its own
|
|
mutual exclusion constraint.
|
|
|
|
### Everything else is an environment input
|
|
|
|
Variables that don't match `control_*` or `q_*` are classified as environment
|
|
inputs (uncontrollable). These are typically continuous predicates abstracted
|
|
to booleans:
|
|
|
|
```
|
|
t_avg_above_min (temperature predicate)
|
|
inv1_holds (safety invariant)
|
|
manual_reset (operator action)
|
|
```
|
|
|
|
### Mutual exclusion encoding
|
|
|
|
FRET uses a single integer variable (`control_mode`) that inherently can only
|
|
hold one value at a time. But ltlsynt works with independent boolean
|
|
propositions. When we decompose `control_mode` into separate booleans
|
|
(`in_mode_shutdown`, `in_mode_heatup`, etc.), we lose the single-valued
|
|
constraint -- the synthesizer could assert multiple modes simultaneously.
|
|
|
|
The mutual exclusion constraint is added automatically by `fret_to_synth.py`
|
|
to restore this invariant. **It is a synthesis encoding artifact, NOT a missing
|
|
FRET requirement.** You do not need to write it in FRET.
|
|
|
|
## Directory Structure
|
|
|
|
```
|
|
fret_processing/
|
|
pwr_hybrid_3.json FRET JSON export
|
|
specs/
|
|
synthesis_config_v3.json Generated synthesis config
|
|
circuits/
|
|
PWR_HYBRID_3_DRC.aag Synthesized AIGER circuit
|
|
diagrams/
|
|
*_states.dot/png/svg State machine diagrams
|
|
scripts/
|
|
fret_to_synth.py FRET-to-ltlsynt converter
|
|
synthesize.sh ltlsynt wrapper
|
|
trace_aiger.py Circuit tracer + visualizer
|
|
aag2dot.py Gate-level circuit diagram
|
|
visualize.sh Visualization wrapper
|
|
.archive/ Old/superseded files
|
|
```
|