# fret_to_synth.py -- FRET Export to Synthesis Config

## Purpose

Converts a FRET JSON export into a synthesis configuration file that
`ltlsynt` (from the Spot library) can consume. Handles the critical encoding
step: FRET's multi-valued mode variables become independent boolean
propositions with automatically generated mutual exclusion constraints.

## Usage

```bash
python3 scripts/fret_to_synth.py <fret_export.json> [output.json]
```

If `output.json` is omitted, writes to `specs/synthesis_config_v3.json`.

## How It Works

### Step 1: Mode Discovery (`discover_modes`)

Regex-scans all `ftInfAUExpanded` (and fallback `ft`) LTL formulas in the
FRET export for patterns matching:

```
(control_GROUPNAME = q_VALUENAME)
```

Returns a dictionary of mode groups:

```python
{
    "control_mode": ["q_heatup", "q_operation", "q_scram", "q_shutdown"],
    "control_pump": ["q_off", "q_running"],  # if present
}
```

This is fully automatic -- no hardcoded variable lists. Adding a new mode in
FRET and re-exporting is all that's needed.

### Step 2: Boolean Encoding (`build_mode_map`)

For each mode group, creates boolean proposition names:

```
control_mode = q_shutdown  -->  in_mode_shutdown
control_mode = q_heatup    -->  in_mode_heatup
control_pump = q_off       -->  in_pump_off
```

The naming rule is: `in_{group_suffix}_{value_suffix}`, where the group
suffix strips `control_` and the value suffix strips `q_`.

Returns a string replacement map used by `encode_ltl` to transform the
FRET LTL formulas.

### Step 3: Variable Classification (`classify_variables`)

Every variable in the FRET semantics is classified:

- **Mode variables** (`control_*`, `q_*`): handled by boolean encoding, excluded
  from explicit input/output lists.
- **Everything else**: classified as an environment input. These are typically
  continuous-domain predicates that have been abstracted to boolean
  (e.g., `t_avg_above_min`, `inv1_holds`).

### Step 4: LTL Encoding (`encode_ltl`)

Simple string replacement of `(control_X = q_Y)` with the corresponding
boolean name. A sanity check ensures no `control_` or `q_` references survive
the transformation -- if a mode value appears in the LTL but wasn't discovered
in Step 1, the script raises an error rather than producing a silent bug.

### Step 5: Mutual Exclusion (`mutual_exclusion_ltl`)

For each mode group, generates an "exactly one active" LTL constraint:

```
G( (a & !b & !c & !d) | (!a & b & !c & !d) | (!a & !b & c & !d) | (!a & !b & !c & d) )
```

This is conjoined with the requirement formulas in the final output.

**Why this is needed:** FRET's `control_mode = q_X` is a single integer
variable -- it inherently holds one value. After decomposition into independent
booleans, the synthesizer could assert `in_mode_heatup = true` AND
`in_mode_scram = true` simultaneously and still satisfy every requirement.
The mutual exclusion constraint prevents this. It is a synthesis encoding
artifact, not a gap in the FRET specifications.

### Step 6: LTL Formula Selection

The script prefers `ftInfAUExpanded` from FRET's semantics object. This is
the future-time LTL formula with:
- Infinite-horizon semantics (no LAST boundary terms)
- Expanded AU (always-until) operators

Fallback is `ft` (the raw future-time formula, which may contain LAST
operators). The `ftInfAUExpanded` form produces cleaner synthesis results
because ltlsynt works over infinite traces.

## Output Format

The generated JSON contains:

| Field | Description |
|---|---|
| `spec_name` | `{PROJECT}_{COMPONENT}` from the FRET export |
| `mode_groups` | Discovered control groups, their values, and boolean names |
| `inputs` | Environment (uncontrollable) variables |
| `outputs` | System (controllable) boolean mode propositions |
| `requirements` | Each FRET requirement with original and encoded LTL |
| `structural_constraints` | Auto-generated mutual exclusion constraints |
| `conjoined_ltl` | All formulas AND'd together, ready for ltlsynt |

## Future Improvements

- **Multi-valued non-mode variables**: Currently assumes all non-mode variables
  are boolean. If FRET exports integer-valued environment variables (e.g.,
  `power_level = 3`), the encoding would need range-based boolean decomposition.

- **Environment assumptions**: No mechanism yet for adding assumptions about the
  environment (e.g., "t_max_exceeded cannot persist forever"). These would need
  to be separated from guarantees in the ltlsynt call (`--ins` assumptions vs.
  `--outs` guarantees). This is important for liveness properties.

- **Liveness constraints**: The old synthesis config had a manual `F(heatup)`
  liveness constraint. Currently there is no automatic detection of which
  requirements imply liveness vs. safety. A future version could parse FRET's
  timing semantics to classify these.

- **Partial observability**: All environment variables are currently assumed
  fully observable. Real reactor instrumentation has sensor noise and delays.
  Extending the pipeline to handle partial observability would require
  belief-state synthesis.