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

3.6 KiB

Raw Blame History

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

# 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 for ltlsynt (brew install spot)
Graphviz 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

3.6 KiB Raw Blame History