Anshuman Singh commited on
Commit Β·
20ad86b
1
Parent(s): cdef82d
Upgrade to Gradio 5.25 (fixes Python 3.13 pydub/audioop incompatibility)
Browse files- README.md +1 -1
- app.py +32 -47
- requirements.txt +0 -1
README.md
CHANGED
|
@@ -4,7 +4,7 @@ emoji: π€
|
|
| 4 |
colorFrom: blue
|
| 5 |
colorTo: red
|
| 6 |
sdk: gradio
|
| 7 |
-
sdk_version: "
|
| 8 |
app_file: app.py
|
| 9 |
pinned: false
|
| 10 |
license: mit
|
|
|
|
| 4 |
colorFrom: blue
|
| 5 |
colorTo: red
|
| 6 |
sdk: gradio
|
| 7 |
+
sdk_version: "5.25.0"
|
| 8 |
app_file: app.py
|
| 9 |
pinned: false
|
| 10 |
license: mit
|
app.py
CHANGED
|
@@ -8,14 +8,12 @@ Change spec priorities β watch the plan change to satisfy the highest-priority
|
|
| 8 |
|
| 9 |
import gradio as gr
|
| 10 |
|
| 11 |
-
from src.grid_world import make_scenario
|
| 12 |
-
from src.automata import parse_spec
|
| 13 |
from src.planner import plan
|
| 14 |
from src.visualize import render_static, render_animation, spec_table_html
|
| 15 |
|
| 16 |
|
| 17 |
-
# ββ Preset spec bundles per scenario βββββββββββββββββββββββββββββββββββββββββ
|
| 18 |
-
|
| 19 |
SCENARIO_SPECS = {
|
| 20 |
"road": [
|
| 21 |
("G(!danger)", "Never cross double line (danger zone)", 80),
|
|
@@ -37,9 +35,9 @@ SCENARIO_SPECS = {
|
|
| 37 |
}
|
| 38 |
|
| 39 |
SCENARIO_DESCRIPTIONS = {
|
| 40 |
-
"road":
|
| 41 |
-
"patrol": "π Warehouse patrol β
|
| 42 |
-
"rescue": "π Rescue mission β
|
| 43 |
}
|
| 44 |
|
| 45 |
|
|
@@ -49,45 +47,47 @@ def run_planning(scenario, r0, r1, r2, r3, animate):
|
|
| 49 |
n_specs = len(specs_raw)
|
| 50 |
rewards_input = [r0, r1, r2, r3][:n_specs]
|
| 51 |
|
| 52 |
-
automata = []
|
| 53 |
-
rewards = []
|
| 54 |
for i, (formula, _, _) in enumerate(specs_raw):
|
| 55 |
try:
|
| 56 |
-
|
| 57 |
-
automata.append(aut)
|
| 58 |
rewards.append(float(rewards_input[i]))
|
| 59 |
except ValueError as e:
|
| 60 |
return None, None, f"<p style='color:red'>Error: {e}</p>"
|
| 61 |
|
| 62 |
-
result
|
| 63 |
-
|
| 64 |
-
|
| 65 |
-
static_img = render_static(grid, result)
|
| 66 |
|
| 67 |
if animate and result.success:
|
| 68 |
-
|
| 69 |
-
return
|
| 70 |
-
|
| 71 |
-
return static_img, None, table_html
|
| 72 |
|
| 73 |
|
| 74 |
def update_scenario_ui(scenario):
|
| 75 |
specs = SCENARIO_SPECS[scenario]
|
| 76 |
desc = SCENARIO_DESCRIPTIONS[scenario]
|
| 77 |
-
n
|
| 78 |
|
| 79 |
-
|
| 80 |
for i in range(4):
|
| 81 |
if i < n:
|
| 82 |
-
_, label,
|
| 83 |
-
|
| 84 |
else:
|
| 85 |
-
|
|
|
|
|
|
|
| 86 |
|
| 87 |
-
return [gr.update(value=f"**{desc}**")] + updates
|
| 88 |
|
|
|
|
|
|
|
|
|
|
|
|
|
| 89 |
|
| 90 |
-
|
|
|
|
| 91 |
|
| 92 |
with gr.Blocks(title="Minimum-Violation LTL Planner", theme=gr.themes.Soft()) as demo:
|
| 93 |
|
|
@@ -113,16 +113,9 @@ the **highest-priority** rules and minimally violates the rest.
|
|
| 113 |
gr.Markdown("### Spec Priorities (higher reward = harder to violate)")
|
| 114 |
|
| 115 |
sliders = []
|
| 116 |
-
|
| 117 |
-
|
| 118 |
-
|
| 119 |
-
_, lbl, val = default_specs[i] if visible else ("", f"Spec {i+1}", 10)
|
| 120 |
-
s = gr.Slider(
|
| 121 |
-
minimum=0, maximum=200, step=5,
|
| 122 |
-
value=val, label=lbl,
|
| 123 |
-
visible=visible,
|
| 124 |
-
)
|
| 125 |
-
sliders.append(s)
|
| 126 |
|
| 127 |
animate_cb = gr.Checkbox(label="Generate animation (GIF)", value=True)
|
| 128 |
plan_btn = gr.Button("βΆ Synthesize Plan", variant="primary")
|
|
@@ -133,7 +126,7 @@ the **highest-priority** rules and minimally violates the rest.
|
|
| 133 |
1. Each spec Οα΅’ becomes a BΓΌchi automaton
|
| 134 |
2. Product automaton = grid Γ autβ Γ autβ Γ ...
|
| 135 |
3. SCCs with accepting states for each spec are found
|
| 136 |
-
4. Max-reward SCC
|
| 137 |
|
| 138 |
π΅ Prefix path π΄ Repeating cycle π£ Start π Robot
|
| 139 |
""")
|
|
@@ -143,8 +136,6 @@ the **highest-priority** rules and minimally violates the rest.
|
|
| 143 |
anim_img = gr.Image(label="Animation (GIF)", type="filepath", height=420)
|
| 144 |
result_md = gr.HTML(label="Spec Satisfaction")
|
| 145 |
|
| 146 |
-
# ββ Event handlers ββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 147 |
-
|
| 148 |
scenario_dd.change(
|
| 149 |
fn=update_scenario_ui,
|
| 150 |
inputs=[scenario_dd],
|
|
@@ -157,15 +148,9 @@ the **highest-priority** rules and minimally violates the rest.
|
|
| 157 |
outputs=[grid_img, anim_img, result_md],
|
| 158 |
)
|
| 159 |
|
| 160 |
-
# Run on load with default scenario
|
| 161 |
demo.load(
|
| 162 |
-
fn=
|
| 163 |
-
outputs=[scenario_desc] + sliders,
|
| 164 |
-
)
|
| 165 |
-
|
| 166 |
-
demo.load(
|
| 167 |
-
fn=lambda: run_planning("road", 80, 50, 30, 10, False),
|
| 168 |
-
outputs=[grid_img, anim_img, result_md],
|
| 169 |
)
|
| 170 |
|
| 171 |
|
|
|
|
| 8 |
|
| 9 |
import gradio as gr
|
| 10 |
|
| 11 |
+
from src.grid_world import make_scenario
|
| 12 |
+
from src.automata import parse_spec
|
| 13 |
from src.planner import plan
|
| 14 |
from src.visualize import render_static, render_animation, spec_table_html
|
| 15 |
|
| 16 |
|
|
|
|
|
|
|
| 17 |
SCENARIO_SPECS = {
|
| 18 |
"road": [
|
| 19 |
("G(!danger)", "Never cross double line (danger zone)", 80),
|
|
|
|
| 35 |
}
|
| 36 |
|
| 37 |
SCENARIO_DESCRIPTIONS = {
|
| 38 |
+
"road": "π Road network β navigate around a danger zone to reach pickup/dropoff areas and a destination.",
|
| 39 |
+
"patrol": "π Warehouse patrol β periodically cover two inspection zones while avoiding a hazardous area.",
|
| 40 |
+
"rescue": "π Rescue mission β reach two survivor sites and periodically return to base, avoiding hazards.",
|
| 41 |
}
|
| 42 |
|
| 43 |
|
|
|
|
| 47 |
n_specs = len(specs_raw)
|
| 48 |
rewards_input = [r0, r1, r2, r3][:n_specs]
|
| 49 |
|
| 50 |
+
automata, rewards = [], []
|
|
|
|
| 51 |
for i, (formula, _, _) in enumerate(specs_raw):
|
| 52 |
try:
|
| 53 |
+
automata.append(parse_spec(formula, label=formula))
|
|
|
|
| 54 |
rewards.append(float(rewards_input[i]))
|
| 55 |
except ValueError as e:
|
| 56 |
return None, None, f"<p style='color:red'>Error: {e}</p>"
|
| 57 |
|
| 58 |
+
result = plan(grid, automata, rewards)
|
| 59 |
+
html = spec_table_html(result)
|
| 60 |
+
static = render_static(grid, result)
|
|
|
|
| 61 |
|
| 62 |
if animate and result.success:
|
| 63 |
+
gif = render_animation(grid, result, fps=3)
|
| 64 |
+
return static, gif, html
|
| 65 |
+
return static, None, html
|
|
|
|
| 66 |
|
| 67 |
|
| 68 |
def update_scenario_ui(scenario):
|
| 69 |
specs = SCENARIO_SPECS[scenario]
|
| 70 |
desc = SCENARIO_DESCRIPTIONS[scenario]
|
| 71 |
+
n = len(specs)
|
| 72 |
|
| 73 |
+
slider_updates = []
|
| 74 |
for i in range(4):
|
| 75 |
if i < n:
|
| 76 |
+
_, label, val = specs[i]
|
| 77 |
+
slider_updates.append(gr.Slider(label=label, value=val, visible=True))
|
| 78 |
else:
|
| 79 |
+
slider_updates.append(gr.Slider(visible=False))
|
| 80 |
+
|
| 81 |
+
return [gr.Markdown(value=f"**{desc}**")] + slider_updates
|
| 82 |
|
|
|
|
| 83 |
|
| 84 |
+
def load_defaults():
|
| 85 |
+
ui = update_scenario_ui("road")
|
| 86 |
+
plan_out = run_planning("road", 80, 50, 30, 10, False)
|
| 87 |
+
return ui + list(plan_out)
|
| 88 |
|
| 89 |
+
|
| 90 |
+
# ββ UI ββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββββ
|
| 91 |
|
| 92 |
with gr.Blocks(title="Minimum-Violation LTL Planner", theme=gr.themes.Soft()) as demo:
|
| 93 |
|
|
|
|
| 113 |
gr.Markdown("### Spec Priorities (higher reward = harder to violate)")
|
| 114 |
|
| 115 |
sliders = []
|
| 116 |
+
for i, (_, lbl, val) in enumerate(SCENARIO_SPECS["road"]):
|
| 117 |
+
sliders.append(gr.Slider(minimum=0, maximum=200, step=5,
|
| 118 |
+
value=val, label=lbl, visible=True))
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 119 |
|
| 120 |
animate_cb = gr.Checkbox(label="Generate animation (GIF)", value=True)
|
| 121 |
plan_btn = gr.Button("βΆ Synthesize Plan", variant="primary")
|
|
|
|
| 126 |
1. Each spec Οα΅’ becomes a BΓΌchi automaton
|
| 127 |
2. Product automaton = grid Γ autβ Γ autβ Γ ...
|
| 128 |
3. SCCs with accepting states for each spec are found
|
| 129 |
+
4. Max-reward SCC β lasso path reconstructed
|
| 130 |
|
| 131 |
π΅ Prefix path π΄ Repeating cycle π£ Start π Robot
|
| 132 |
""")
|
|
|
|
| 136 |
anim_img = gr.Image(label="Animation (GIF)", type="filepath", height=420)
|
| 137 |
result_md = gr.HTML(label="Spec Satisfaction")
|
| 138 |
|
|
|
|
|
|
|
| 139 |
scenario_dd.change(
|
| 140 |
fn=update_scenario_ui,
|
| 141 |
inputs=[scenario_dd],
|
|
|
|
| 148 |
outputs=[grid_img, anim_img, result_md],
|
| 149 |
)
|
| 150 |
|
|
|
|
| 151 |
demo.load(
|
| 152 |
+
fn=load_defaults,
|
| 153 |
+
outputs=[scenario_desc] + sliders + [grid_img, anim_img, result_md],
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 154 |
)
|
| 155 |
|
| 156 |
|
requirements.txt
CHANGED
|
@@ -1,4 +1,3 @@
|
|
| 1 |
-
pyaudioop
|
| 2 |
matplotlib>=3.7.0
|
| 3 |
networkx>=3.0
|
| 4 |
numpy>=1.24.0
|
|
|
|
|
|
|
| 1 |
matplotlib>=3.7.0
|
| 2 |
networkx>=3.0
|
| 3 |
numpy>=1.24.0
|