# synthesize.sh -- ltlsynt Reactive Synthesis Wrapper

## Purpose

Reads a synthesis configuration JSON and invokes `ltlsynt` (from the Spot
library) to produce a reactive controller as an AIGER circuit. This is the
step where temporal logic specifications become a concrete implementation.

## Usage

```bash
bash scripts/synthesize.sh <synthesis_config.json> [output_dir]
```

- `synthesis_config.json`: output of `fret_to_synth.py`
- `output_dir`: where to write the `.aag` file (default: `circuits/`)

## How It Works

### Parameter Extraction

A small inline Python script reads the JSON config and extracts:

- `INPUTS`: comma-separated list of environment variables (uncontrollable)
- `OUTPUTS`: comma-separated list of system variables (controllable)
- `LTL_FORMULA`: the conjoined LTL specification
- `SPEC_NAME`: used for the output filename

### The ltlsynt Call

```bash
ltlsynt -f "$LTL_FORMULA" \
  --ins="$INPUTS" \
  --outs="$OUTPUTS" \
  --aiger=both+ud+dc \
  --simplify=bwoa-sat
```

**Flags explained:**

| Flag | Meaning |
|---|---|
| `-f` | LTL formula (the specification) |
| `--ins` | Input (environment/uncontrollable) propositions |
| `--outs` | Output (system/controllable) propositions |
| `--aiger=both+ud+dc` | Output as ASCII AIGER with both latches and gates, using unit delays and don't-cares for optimization |
| `--simplify=bwoa-sat` | Best simplification: bounded width with SAT-based optimization. Produces the smallest circuit |

### The Two-Player Game

Reactive synthesis frames controller design as a two-player game:

- **Player 1 (Environment)**: controls the `--ins` variables. Assumed to be
  adversarial -- the synthesizer must find a strategy that wins against ALL
  possible environment behaviors, including worst-case.

- **Player 2 (Controller)**: controls the `--outs` variables. The synthesizer
  searches for a strategy (a Mealy machine) such that no matter what Player 1
  does, the LTL specification is satisfied.

**Why adversarial?** Because we need a controller that works in ALL operating
conditions, not just typical ones. If the environment CAN violate a safety
invariant, the synthesizer assumes it WILL, and the controller must handle it.

This is why the old PWR_Hybrid specs produced a degenerate controller: the
environment could force `t_max_exceeded` every step, triggering irrecoverable
SCRAM. The only winning strategy was to SCRAM immediately. The new specs
have proper guard conditions that give the controller legal responses to every
environment move.

### Realizability

ltlsynt outputs one of two results:

- **REALIZABLE**: A winning strategy exists. The AIGER circuit is printed
  after the `REALIZABLE` line. The script strips this line and writes the
  circuit to `{output_dir}/{spec_name}.aag`.

- **UNREALIZABLE**: No controller can satisfy the specification against all
  possible environment behaviors. This means the specs have a fundamental
  conflict. Use FRET's realizability checking and counterexample traces to
  diagnose which requirements conflict.

### Output: AIGER Format

The `.aag` (ASCII AIGER) file is a text-based hardware description:

```
aag M I L O A           Header: Max-var, Inputs, Latches, Outputs, ANDs
<input literals>        One per line, even numbers (2, 4, 6, ...)
<latch definitions>     current_lit next_lit (state registers)
<output literals>       Which literals are outputs
<AND gates>             lhs rhs0 rhs1 (lhs = rhs0 AND rhs1)
<symbol table>          i0 name, o0 name, etc.
```

**Literal encoding:** Variable `n` has literal `2n` (positive) and `2n+1`
(negated). Literal `0` = constant FALSE, literal `1` = constant TRUE.
XOR-ing a literal with 1 flips its polarity.

**Latches** are 1-bit registers that initialize to 0. With `L` latches,
the controller has up to `2^L` internal states. The circuit is a Mealy
machine: outputs depend on both current state (latches) and current inputs.

## Future Improvements

- **Environment assumptions**: ltlsynt supports `--from-ltlf` for finite
  traces and can separate assumptions from guarantees. Adding support for
  environment assumptions (e.g., fairness constraints like "the environment
  won't hold t_max_exceeded forever") would expand the class of realizable
  specifications.

- **Decomposed synthesis**: For large specs, monolithic synthesis can be
  expensive. Compositional synthesis (synthesizing each mode's controller
  separately and composing them) could improve scalability.

- **Alternative output formats**: The AIGER circuit could be translated to
  Verilog, VHDL, or Simulink/Stateflow for integration with existing
  control system toolchains.

- **Timeout handling**: Currently no timeout on the ltlsynt call. Very
  complex specifications can take hours. Adding a configurable timeout
  with a clear error message would improve usability.