cebf8c167a
Folds three previously-separate pieces into one preliminary-example repo for the HAHACS thesis: - thesis/ (submodule) → gitea Thesis.git — the PhD proposal - fret-pipeline/ — FRET requirements to AIGER controller (was ~/Documents/fret_processing/; prior single-commit history abandoned per user decision) - plant-model/ — 10-state PKE + lumped T/H PWR model (was ~/Documents/PKE_Playground/; never version-controlled before) - presentations/2026DICE/ (submodule) → gitea 2026DICE.git - reachability/, hardware/ — empty placeholders for Thrust 3 and HIL - docs/architecture.md — how the discrete and continuous layers compose - claude_memory/ — session notes and scratch knowledge pattern Plant model refactored to thesis naming (x, plant, u, ref); pke_th_rhs now takes u as an explicit arg instead of reading rho_ext from the params struct. First two controllers built to the contract u = ctrl_<mode>(t, x, plant, ref): ctrl_null (baseline) and ctrl_operation (stabilizing, proportional on T_avg). Validated under a 100% -> 80% Q_sg step: ctrl_operation reduces steady-state T_avg drift ~47% vs. the unforced plant. Root CLAUDE.md emphasizes that CLAUDE.md files are living documents and that any knowledge not captured before a session ends is lost forever; claude_memory/ holds the session-level notes that haven't stabilized enough to graduate into a CLAUDE.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
81 lines
2.3 KiB
Bash
Executable File
81 lines
2.3 KiB
Bash
Executable File
#!/usr/bin/env bash
|
|
# Synthesize a controller from a FRET synthesis config using ltlsynt (Spot).
|
|
#
|
|
# Usage: ./scripts/synthesize.sh specs/synthesis_config.json [output_dir]
|
|
#
|
|
# Reads the synthesis_config.json produced by parse_fret_json.py and
|
|
# runs ltlsynt to produce an AIGER circuit.
|
|
|
|
set -euo pipefail
|
|
|
|
CONFIG="${1:?Usage: $0 <synthesis_config.json> [output_dir]}"
|
|
OUTPUT_DIR="${2:-circuits}"
|
|
|
|
if ! command -v ltlsynt &>/dev/null; then
|
|
echo "Error: ltlsynt not found. Install with: brew install spot"
|
|
exit 1
|
|
fi
|
|
|
|
mkdir -p "$OUTPUT_DIR"
|
|
|
|
# Extract synthesis parameters from config
|
|
eval "$(python3 -c "
|
|
import json, sys, shlex
|
|
|
|
config = json.load(open(sys.argv[1]))
|
|
inputs = config['inputs']
|
|
outputs = config['outputs']
|
|
ltl = config.get('conjoined_ltl')
|
|
spec_name = config['spec_name']
|
|
|
|
if not ltl:
|
|
print('echo \"Error: no conjoined LTL formula in config\"; exit 1')
|
|
sys.exit(0)
|
|
if not outputs:
|
|
print('echo \"Error: no output variables defined\"; exit 1')
|
|
sys.exit(0)
|
|
|
|
print(f'SPEC_NAME={shlex.quote(spec_name)}')
|
|
print(f'INPUTS={shlex.quote(\",\".join(inputs))}')
|
|
print(f'OUTPUTS={shlex.quote(\",\".join(outputs))}')
|
|
print(f'LTL_FORMULA={shlex.quote(ltl)}')
|
|
" "$CONFIG")"
|
|
|
|
AAG_FILE="$OUTPUT_DIR/${SPEC_NAME}.aag"
|
|
|
|
echo "=== ltlsynt Reactive Synthesis ==="
|
|
echo "Spec: $SPEC_NAME"
|
|
echo "Inputs: $INPUTS"
|
|
echo "Outputs: $OUTPUTS"
|
|
echo "Formula: ${LTL_FORMULA:0:200}..."
|
|
echo ""
|
|
echo "Running ltlsynt..."
|
|
|
|
# Run ltlsynt
|
|
# -f: LTL formula
|
|
# --ins: uncontrollable (input/environment) propositions
|
|
# --outs: controllable (output/system) propositions
|
|
# --aiger: output as AIGER circuit
|
|
# --simplify=bwoa-sat: best simplification
|
|
SYNTH_OUTPUT=$(ltlsynt -f "$LTL_FORMULA" --ins="$INPUTS" --outs="$OUTPUTS" --aiger=both+ud+dc --simplify=bwoa-sat 2>&1) || true
|
|
|
|
if echo "$SYNTH_OUTPUT" | head -1 | grep -q "^REALIZABLE"; then
|
|
echo ""
|
|
echo "Result: REALIZABLE"
|
|
# Strip the REALIZABLE line and write the AIGER circuit
|
|
echo "$SYNTH_OUTPUT" | tail -n +2 > "$AAG_FILE"
|
|
LINES=$(wc -l < "$AAG_FILE")
|
|
echo "Circuit written to: $AAG_FILE ($LINES lines)"
|
|
elif echo "$SYNTH_OUTPUT" | head -1 | grep -q "^UNREALIZABLE"; then
|
|
echo ""
|
|
echo "Result: UNREALIZABLE"
|
|
echo "The specification cannot be implemented as a controller."
|
|
echo "$SYNTH_OUTPUT"
|
|
exit 1
|
|
else
|
|
echo ""
|
|
echo "Error: unexpected ltlsynt output:"
|
|
echo "$SYNTH_OUTPUT"
|
|
exit 1
|
|
fi
|