PWR-HYBRID-3/fret-pipeline/.archive/abstract_lpc.py

#!/usr/bin/env python3
"""Abstract the LPC spec into boolean LTL for reactive synthesis.

The LPC spec uses real-valued variables (kias/kgs) and enumerated modes.
This script creates a boolean abstraction suitable for ltlsynt.

Speed regions (kias = kgs, so one variable):
  A: speed <= 20   (hover zone)
  B: 20 < speed <= 30
  C: 30 < speed <= 40
  D: 40 < speed <= 90
  E: 90 < speed <= 100
  F: speed > 100

Modes (lift_mode):
  tb:  thrust_borne
  stb: semi_thrust_borne
  swb: semi_wing_borne
  wb:  wing_borne

The environment controls speed (within adjacency constraints).
The controller chooses the mode.
"""

import json
from pathlib import Path


def build_lpc_spec():
    regions = ['a', 'b', 'c', 'd', 'e', 'f']
    modes = ['tb', 'stb', 'swb', 'wb']

    # Helper: exactly one of a list is true
    def exactly_one(vars):
        # At least one
        at_least = ' | '.join(vars)
        # At most one (pairwise exclusion)
        pairs = []
        for i in range(len(vars)):
            for j in range(i + 1, len(vars)):
                pairs.append(f'(!{vars[i]} | !{vars[j]})')
        at_most = ' & '.join(pairs)
        return f'({at_least}) & {at_most}'

    region_vars = [f'r_{r}' for r in regions]
    mode_vars = [f'm_{m}' for m in modes]

    # === ENVIRONMENT ASSUMPTIONS ===
    assumptions = []

    # Exactly one speed region (always)
    assumptions.append(f'G({exactly_one(region_vars)})')

    # Initial speed: region F (kias = 120 > 100)
    assumptions.append('r_f')

    # Speed adjacency: can only move to adjacent region per tick
    # (from the derivative constraint: |delta kias| <= 10 per tick)
    adjacency = {
        'r_a': ['r_a', 'r_b'],
        'r_b': ['r_a', 'r_b', 'r_c'],
        'r_c': ['r_b', 'r_c', 'r_d'],
        'r_d': ['r_c', 'r_d', 'r_e'],
        'r_e': ['r_d', 'r_e', 'r_f'],
        'r_f': ['r_e', 'r_f'],
    }
    for region, neighbors in adjacency.items():
        next_options = ' | '.join(f'X({n})' for n in neighbors)
        assumptions.append(f'G({region} -> ({next_options}))')

    # hover_control_mode <=> speed <= 20 (region A)
    # We absorb hover into r_a directly in the guarantees

    # === CONTROLLER GUARANTEES ===
    guarantees = []

    # Exactly one mode (always)
    guarantees.append(f'G({exactly_one(mode_vars)})')

    # Initial mode: wing_borne (since kias = 120 >= 90)
    # LPC_INIT_LIFT_MODE: lift_mode = wb <=> kias >= 90, and kias = 120
    guarantees.append('m_wb')

    # === MODE TRANSITIONS (from FRET requirements) ===

    # LPC_WB_STAY_ON_NEXT: While wb & kias > 90 -> next wb
    # kias > 90 means region E or F
    guarantees.append('G((m_wb & (r_e | r_f)) -> X(m_wb))')

    # LPC_WB_TO_SWB: Upon wb & kias <= 90 -> next swb
    # kias <= 90 means region A-D
    guarantees.append('G((m_wb & (r_a | r_b | r_c | r_d)) -> X(m_swb))')

    # LPC_SWB_STAY_ON_NEXT: While swb & kias <= 100 & kias > 30 -> next swb
    # 30 < kias <= 100 means region D or E
    guarantees.append('G((m_swb & (r_d | r_e)) -> X(m_swb))')

    # LPC_SWB_TO_WB: Upon swb & kias > 100 -> next wb
    # kias > 100 means region F
    guarantees.append('G((m_swb & r_f) -> X(m_wb))')

    # LPC_SWB_TO_STB: Upon swb & kias <= 30 -> next stb
    # kias <= 30 means region A or B
    guarantees.append('G((m_swb & (r_a | r_b)) -> X(m_stb))')

    # LPC_STB_STAY_ON_NEXT: While stb & kias <= 40 & (kgs > 20 | !hover)
    # kias <= 40 means region A-C; kgs > 20 | !hover means NOT region A
    # So: stb & (region B or C) -> next stb
    guarantees.append('G((m_stb & (r_b | r_c)) -> X(m_stb))')

    # LPC_STB_TO_SWB: Upon stb & kias > 40 -> next swb
    # kias > 40 means region D-F
    guarantees.append('G((m_stb & (r_d | r_e | r_f)) -> X(m_swb))')

    # LPC_STB_TO_TB: Upon stb & hover & kgs <= 20 -> next tb
    # hover & kgs <= 20 means region A
    guarantees.append('G((m_stb & r_a) -> X(m_tb))')

    # LPC_TB_STAY_ON_NEXT: While tb & kgs <= 20 & hover -> next tb
    # region A
    guarantees.append('G((m_tb & r_a) -> X(m_tb))')

    # LPC_TB_TO_STB: Upon tb & (!hover | kgs > 20) -> next stb
    # NOT region A
    guarantees.append('G((m_tb & (r_b | r_c | r_d | r_e | r_f)) -> X(m_tb | m_stb))')
    # Wait, the original says -> next stb. Let me fix:
    # Actually: Upon tb & (!hover | kgs > 20) -> next stb
    # !hover | kgs > 20 means NOT in region A
    guarantees[-1] = 'G((m_tb & !r_a) -> X(m_stb))'

    # Note: we skip LPC_REACH_HOVER_06 and _12 (bounded temporal F[0,n])
    # ltlsynt doesn't support bounded-F natively

    # === BUILD FORMULA ===
    # assume-guarantee: assumptions -> guarantees
    assume_str = ' & '.join(f'({a})' for a in assumptions)
    guarantee_str = ' & '.join(f'({g})' for g in guarantees)
    formula = f'({assume_str}) -> ({guarantee_str})'

    inputs = region_vars
    outputs = mode_vars

    return {
        '_comment': 'Boolean abstraction of LPC lift-mode controller. Assumes -> Guarantees form.',
        'spec_name': 'LPC_mini',
        'source_file': 'specs/LPC_mini_reqts_and_vars.json',
        'inputs': inputs,
        'outputs': outputs,
        'assumptions': assumptions,
        'guarantees': guarantees,
        'conjoined_ltl': formula,
        'abstraction_notes': {
            'speed_regions': {
                'r_a': 'speed <= 20 (hover zone)',
                'r_b': '20 < speed <= 30',
                'r_c': '30 < speed <= 40',
                'r_d': '40 < speed <= 90',
                'r_e': '90 < speed <= 100',
                'r_f': 'speed > 100',
            },
            'modes': {
                'm_tb': 'thrust_borne',
                'm_stb': 'semi_thrust_borne',
                'm_swb': 'semi_wing_borne',
                'm_wb': 'wing_borne',
            },
            'skipped_requirements': [
                'LPC_REACH_HOVER_06 (bounded temporal F[0,6])',
                'LPC_REACH_HOVER_12 (bounded temporal F[0,12])',
                'LPC_KIAS_DERIVATIVE (absorbed into adjacency constraint)',
                'LPC_KIAS_KGS (absorbed - single speed variable)',
                'LPC_INIT_KIAS (absorbed into initial region)',
                'LPC_KIAS_0 (trivially satisfied)',
                'LPC_INIT_HOVER_MODE (absorbed - hover = region A)',
            ],
        },
    }


if __name__ == '__main__':
    config = build_lpc_spec()
    out = Path('specs/lpc_synthesis_config.json')
    out.write_text(json.dumps(config, indent=2) + '\n')

    print(f'LPC Boolean Abstraction')
    print(f'Inputs  ({len(config["inputs"])}): {", ".join(config["inputs"])}')
    print(f'Outputs ({len(config["outputs"])}): {", ".join(config["outputs"])}')
    print(f'\nAssumptions ({len(config["assumptions"])}):')
    for a in config['assumptions']:
        print(f'  {a}')
    print(f'\nGuarantees ({len(config["guarantees"])}):')
    for g in config['guarantees']:
        print(f'  {g}')
    print(f'\nSkipped: {len(config["abstraction_notes"]["skipped_requirements"])} requirements')
    print(f'Config written to: {out}')