app.py

"""
Minimum-Violation LTL Planning — Interactive Demo
Reproduces: Tumova et al., "Minimum-Violation LTL Planning with Conflicting
Specifications", ACC 2013 (arXiv:1303.3679)

Change spec priorities → watch the plan change to satisfy the highest-priority rules.
"""

import gradio as gr

from src.grid_world import make_scenario
from src.automata import parse_spec
from src.planner import plan
from src.visualize import render_static, render_animation, spec_table_html


SCENARIO_SPECS = {
    "road": [
        ("G(!danger)",  "Never cross double line (danger zone)", 80),
        ("GF(zone_a)",  "Periodically visit pickup zone A",      50),
        ("GF(zone_b)",  "Periodically visit dropoff zone B",     30),
        ("F(goal)",     "Eventually reach the goal",             10),
    ],
    "patrol": [
        ("G(!danger)",  "Stay away from danger zones",    100),
        ("GF(zone_a)",  "Patrol zone A repeatedly",        60),
        ("GF(zone_b)",  "Patrol zone B repeatedly",        40),
    ],
    "rescue": [
        ("G(!danger)",  "Avoid hazardous areas",           90),
        ("F(zone_a)",   "Reach survivor site A",           70),
        ("F(zone_b)",   "Reach survivor site B",           50),
        ("GF(zone_c)",  "Return to base (zone C) always",  20),
    ],
}

SCENARIO_DESCRIPTIONS = {
    "road":   "🚗 Road network — navigate around a danger zone to reach pickup/dropoff areas and a destination.",
    "patrol": "🏭 Warehouse patrol — periodically cover two inspection zones while avoiding a hazardous area.",
    "rescue": "🚁 Rescue mission — reach two survivor sites and periodically return to base, avoiding hazards.",
}


def run_planning(scenario, r0, r1, r2, r3, animate):
    grid = make_scenario(scenario)
    specs_raw = SCENARIO_SPECS[scenario]
    n_specs = len(specs_raw)
    rewards_input = [r0, r1, r2, r3][:n_specs]

    automata, rewards = [], []
    for i, (formula, _, _) in enumerate(specs_raw):
        try:
            automata.append(parse_spec(formula, label=formula))
            rewards.append(float(rewards_input[i]))
        except ValueError as e:
            return None, None, f"<p style='color:red'>Error: {e}</p>"

    result   = plan(grid, automata, rewards)
    html     = spec_table_html(result)
    static   = render_static(grid, result)

    if animate and result.success:
        gif = render_animation(grid, result, fps=3)
        # Embed as base64 so Gradio 5.x HTML component plays it natively
        import base64
        with open(gif, "rb") as f:
            b64 = base64.b64encode(f.read()).decode()
        gif_html = (
            f"<img src='data:image/gif;base64,{b64}' "
            f"style='max-width:100%;border-radius:8px'/>"
        )
        return static, gif_html, html
    return static, "", html


def update_scenario_ui(scenario):
    specs = SCENARIO_SPECS[scenario]
    desc  = SCENARIO_DESCRIPTIONS[scenario]
    n     = len(specs)

    slider_updates = []
    for i in range(4):
        if i < n:
            _, label, val = specs[i]
            slider_updates.append(gr.Slider(label=label, value=val, visible=True))
        else:
            slider_updates.append(gr.Slider(visible=False))

    return [gr.Markdown(value=f"**{desc}**")] + slider_updates


def load_defaults():
    ui   = update_scenario_ui("road")
    plan_out = run_planning("road", 80, 50, 30, 10, False)
    return ui + list(plan_out)


# ── UI ────────────────────────────────────────────────────────────────────────

with gr.Blocks(title="Minimum-Violation LTL Planner", theme=gr.themes.Soft()) as demo:

    gr.Markdown("""
# Minimum-Violation LTL Planning
**Reproducing:** Tumova et al., *"Minimum-Violation LTL Planning with Conflicting Specifications"*, ACC 2013

When robot specs conflict, instead of failing, this planner finds the path that satisfies
the **highest-priority** rules and minimally violates the rest.

> **Try it:** drag the reward sliders to swap priorities — watch the planned path change.
""")

    with gr.Row():
        with gr.Column(scale=1):
            scenario_dd = gr.Dropdown(
                choices=["road", "patrol", "rescue"],
                value="road",
                label="Scenario",
            )
            scenario_desc = gr.Markdown("**Loading...**")

            gr.Markdown("### Spec Priorities (higher reward = harder to violate)")

            sliders = []
            for i, (_, lbl, val) in enumerate(SCENARIO_SPECS["road"]):
                sliders.append(gr.Slider(minimum=0, maximum=200, step=5,
                                         value=val, label=lbl, visible=True))

            animate_cb = gr.Checkbox(label="Generate animation (GIF)", value=True)
            plan_btn   = gr.Button("▶  Synthesize Plan", variant="primary")

            gr.Markdown("""
---
**How it works:**
1. Each spec φᵢ becomes a Büchi automaton
2. Product automaton = grid × aut₁ × aut₂ × ...
3. SCCs with accepting states for each spec are found
4. Max-reward SCC → lasso path reconstructed

🔵 Prefix path &nbsp;&nbsp; 🔴 Repeating cycle &nbsp;&nbsp; 🟣 Start &nbsp;&nbsp; 🟠 Robot
""")

        with gr.Column(scale=2):
            grid_img  = gr.Image(label="Planned Path", type="pil", height=420)
            anim_img  = gr.HTML(label="Animation (GIF)")
            result_md = gr.HTML(label="Spec Satisfaction")

    scenario_dd.change(
        fn=update_scenario_ui,
        inputs=[scenario_dd],
        outputs=[scenario_desc] + sliders,
    )

    plan_btn.click(
        fn=run_planning,
        inputs=[scenario_dd] + sliders + [animate_cb],
        outputs=[grid_img, anim_img, result_md],
    )

    demo.load(
        fn=load_defaults,
        outputs=[scenario_desc] + sliders + [grid_img, anim_img, result_md],
    )


if __name__ == "__main__":
    demo.launch()