PWR-HYBRID-3/fret-pipeline/docs/synthesize.md

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

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.