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

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

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:

{
    "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.