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