From 44cc193829f7f5753ead3a251162f14ef0a691f8 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Mon, 20 Apr 2026 21:48:08 -0400 Subject: [PATCH] app: Pluto.jl predicate explorer v1 (read-only) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The hybrid-systems-group tab for FRET, as a stand-alone Pluto notebook. Reads reachability/predicates.json and renders: - Plant-derived constants (T_c0, T_standby, etc.) - All operational deadbands with concretization - All safety limits as one-sided halfspaces with meanings - Mode invariants (inv1_holds, inv2_holds) as conjunctions - Per-mode entry/safe/exit/time tables - 2D projection of operating polytope (T_avg x n) - Reach-traceability table — what's covered, by which artifact - Edit-UX preview with sliders that don't actually write back Run with: cd app julia --project=. -e 'using Pkg; Pkg.instantiate()' # first time julia --project=. -e 'using Pluto; Pluto.run()' V2 will add write-back to predicates.json. V3 (the dream) is FRET-spec driven derivation of halfspaces from a structured vocabulary of physical bounds. Co-Authored-By: Claude Opus 4.7 (1M context) --- app/.gitignore | 1 + app/Project.toml | 10 ++ app/README.md | 65 +++++++ app/predicate_explorer.jl | 360 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 436 insertions(+) create mode 100644 app/.gitignore create mode 100644 app/Project.toml create mode 100644 app/README.md create mode 100644 app/predicate_explorer.jl diff --git a/app/.gitignore b/app/.gitignore new file mode 100644 index 0000000..ba39cc5 --- /dev/null +++ b/app/.gitignore @@ -0,0 +1 @@ +Manifest.toml diff --git a/app/Project.toml b/app/Project.toml new file mode 100644 index 0000000..3b26fbb --- /dev/null +++ b/app/Project.toml @@ -0,0 +1,10 @@ +authors = ["Dane Sabo "] + +[deps] +JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6" +Pluto = "c3e4b0f8-55cb-11ea-2926-15256bba5781" +PlutoUI = "7f904dfe-b85e-4ff6-b463-dae2292396a8" +Plots = "91a5bcdd-55d7-5caf-9e0b-520d859cae80" + +[compat] +julia = "1.10" diff --git a/app/README.md b/app/README.md new file mode 100644 index 0000000..30918fc --- /dev/null +++ b/app/README.md @@ -0,0 +1,65 @@ +# app — Predicate Explorer (Pluto.jl) + +A local-server visual companion to `reachability/predicates.json`. Maps +the FRET-spec boolean predicates to their numerical halfspaces over the +10-state continuous vector, shows mode invariants as conjunctions of +named safety limits, and previews a UI for editing them. + +**v1: read-only.** Sliders display in the edit panel but do not write +back to the JSON. v2 will add live write-through. v3 (the dream) will +derive halfspaces automatically from the FRET spec. + +This is the FRET-adjacent piece — the "hybrid-systems group tab" we +talked about. Stand-alone for now; integration into the upstream FRET +UI is a later story. + +## Run + +First time: + +```bash +cd app +julia --project=. -e 'using Pkg; Pkg.instantiate()' +``` + +Subsequent: + +```bash +julia --project=. -e 'using Pluto; Pluto.run()' +``` + +A browser window opens (default `http://localhost:1234`). Pick +`predicate_explorer.jl` from the file list. The notebook is reactive — +edit any cell, dependent cells re-run. + +## What you can do today (v1) + +- Inspect every operational deadband, safety limit, mode invariant, + and mode boundary. +- See the boolean ↔ continuous mapping for each predicate. +- View a 2D projection (T_avg × n) showing the operating polytope. +- Read the reach-status traceability table — which artifact has tried + to discharge which obligation, with link. +- Move sliders to feel out the editing workflow. + +## What lands in v2 + +- Sliders write back to `predicates.json` with an "are you sure" gate. +- Diff view: pending changes vs.\ the on-disk version. +- Re-run reach scripts in-place from the notebook. + +## What's the dream (v3) + +- The FRET spec at `../fret-pipeline/pwr_hybrid_3.json` declares + predicate names without numerical concretization. Could we use a + structured ontology of physical bounds (fuel limits, trip setpoints, + rate limits) plus the FRET text to *derive* the concretization? +- Round-tripping changes back into the FRET model so the synthesis side + stays consistent. + +## Caveats + +- Pluto notebooks aren't great in version control — they're long files + with cell UUIDs and order metadata. The notebook is committed because + it's small and the cell order matters. +- Manifest.toml is gitignored; regenerate locally. diff --git a/app/predicate_explorer.jl b/app/predicate_explorer.jl new file mode 100644 index 0000000..5ed5371 --- /dev/null +++ b/app/predicate_explorer.jl @@ -0,0 +1,360 @@ +### A Pluto.jl notebook ### +# v0.19.40 + +using Markdown +using InteractiveUtils + +# This Pluto notebook uses @bind for interactivity. The macro is defined locally +# so the file remains a valid standalone Julia script when Pluto isn't running. +macro bind(def, element) + #= none:1 =# quote + local iv = try + Base.loaded_modules[Base.PkgId(Base.UUID("6e696c72-6542-2067-7265-42206c756150"), "AbstractPlutoDingetjes")].Bonds.initial_value + catch + b -> missing + end + local el = $(esc(element)) + global $(esc(def)) = Core.applicable(Base.get, el) ? Base.get(el) : iv(el) + el + end +end + +# ╔═╡ 9d14e486-1faa-45a9-b235-6367a039f9da +begin + using Pkg + Pkg.activate(@__DIR__) + using JSON + using PlutoUI + using Plots + gr() +end + +# ╔═╡ 08e80248-89fe-4639-b55c-f10d96de6c31 +md""" +# 🦎 Predicate Explorer + +> *Hybrid-systems extension to FRET — the bridge between boolean predicates +> and continuous-state halfspaces.* + +This notebook is the visual companion to `reachability/predicates.json`. +Each FRET-spec predicate (a boolean condition over named variables) maps to a +**numerical halfspace** over the 10-state continuous vector +``x = [n,\, C_1, \ldots, C_6,\, T_f,\, T_c,\, T_{\mathrm{cold}}]``. + +Use it to: +- Inspect what each predicate *physically means*. +- See how mode invariants compose from named safety limits. +- Trace which reach artifact has tried to discharge each obligation. +- Sketch edits in a UI that mirrors the JSON structure (read-only v1 — edits + do not persist). + +The data behind everything below is `../reachability/predicates.json`. +Edit the JSON, restart this notebook, results re-render. +""" + +# ╔═╡ d7cadb58-e7c4-4701-8fcb-380f1e948d42 +md""" +## 1 · Source of truth — load `predicates.json` +""" + +# ╔═╡ c995a73a-c07e-415b-abe8-57abaf9f4b46 +begin + pred_path = joinpath(@__DIR__, "..", "reachability", "predicates.json") + pred_raw = JSON.parsefile(pred_path) + md"Loaded `$(relpath(pred_path))`. Top-level keys: $(join(sort(collect(keys(pred_raw))), ", "))." +end + +# ╔═╡ 48f4bec1-ac48-4318-ba6e-92dbf80a7b2d +md""" +## 2 · Plant-derived constants + +These are computed once from `pke_params()` (the plant model in `../code/`) +and used as the basis for every halfspace. + +| Symbol | Meaning | Value | +|---|---|---| +| `T_c0` | Operating-point average coolant T | $(round(308.349; digits=2)) °C | +| `T_f0` | Operating-point fuel T | $(round(328.349; digits=2)) °C | +| `T_cold0` | Operating-point cold-leg T | 290.00 °C | +| `T_standby` | Hot-standby T | $(round(308.349 + pred_raw["derived"]["T_standby_offset_C"]; digits=2)) °C | + +Hot standby is defined as `T_c0 - 60 °F = T_c0 - 33.33 °C`. Source-of-truth +constants live under the `derived` key in the JSON. +""" + +# ╔═╡ 7ec2cd9d-5c5c-47d7-aa3c-189091b97204 +md""" +## 3 · Operational deadbands + +Soft bands used by the **DRC** to switch modes. These are *not* safety +properties — violating them triggers a mode change or operator alert, +not damage. + +| Predicate | Meaning | +|---|---| +$(join(["| `$name` | $(get(entry, "meaning", "")) |" for (name, entry) in pred_raw["operational_deadbands"] if !startswith(name, "_")], "\n")) +""" + +# ╔═╡ e99c4c2b-7d29-49a4-a474-047f204e331f +md""" +### Concretization of `t_avg_in_range` + +> *"Average coolant in tight operating band — used for heatup → operation transition."* + +In FRET this is the boolean predicate `t_avg_in_range`. In the continuous +state space it concretizes to the box + +``` +T_c0 - 2.778 ≤ T_c ≤ T_c0 + 2.778 (°C) +``` + +Halfwidth = 2.778 °C ≈ 5 °F (typical PWR T_avg deadband). The two halfspace +rows live as `state_index = 9` (which is `T_c`) with coefficients ±1 and the +appropriate offset. +""" + +# ╔═╡ 408432c8-2cc6-4505-8623-9f5614a72c4d +md""" +## 4 · Safety limits — the hard constraints + +These are **one-sided halfspaces** corresponding to physical damage mechanisms +or reactor-trip setpoints. Asymmetric: the plant is not equally vulnerable on +both sides of the setpoint. These are what reach analyses target. +""" + +# ╔═╡ 0ef6cd25-7f9c-4d64-afdb-ffe8af1ac967 +begin + safety_rows = [] + for (name, entry) in pred_raw["safety_limits"] + startswith(name, "_") && continue + meaning = get(entry, "meaning", "") + concret = get(entry, "concretization", "") + push!(safety_rows, (name=name, meaning=meaning, concretization=concret)) + end + md_table = "| Limit | What it protects | Concretization |\n|---|---|---|\n" + for r in safety_rows + md_table *= "| `$(r.name)` | $(r.meaning) | `$(r.concretization)` |\n" + end + Markdown.parse(md_table) +end + +# ╔═╡ 68b1c7bf-c498-41a9-a435-1332c8154035 +md""" +## 5 · Mode invariants — conjunctions of safety limits + +`inv1_holds` (heatup) and `inv2_holds` (operation) are safety envelopes, +declared as a conjunction of named entries from the safety-limits group. +Changing a limit propagates automatically. +""" + +# ╔═╡ 06be0c87-2a28-4ab3-9fa1-ccde3a9b70d9 +begin + function render_invariant(name) + haskey(pred_raw["mode_invariants"], name) || return md"_(not present)_" + entry = pred_raw["mode_invariants"][name] + components = entry["conjunction_of"] + components = isa(components, String) ? [components] : components + comp_md = join(["- `$c`" for c in components], "\n") + Markdown.parse( + "**`$name`**: $(get(entry, "meaning", ""))\n\nConjunction of:\n\n$comp_md\n" + ) + end + render_invariant("inv1_holds") +end + +# ╔═╡ 8a24ff1e-0afb-4707-89d7-fa50e3b74dbd +render_invariant("inv2_holds") + +# ╔═╡ e67f3259-ce97-4bf5-9e63-8f3aef7c6c56 +md""" +## 6 · Mode boundaries — entry / safe / exit / time + +For each DRC mode, the reach-analysis triple: where does state start, where +must it stay, where must it land, by when. **Equilibrium modes** have no +T_max (forever-invariance is the obligation). **Transition modes** have +both T_min and T_max (reach-avoid is the obligation). +""" + +# ╔═╡ a17586e3-b8f5-4608-950b-69ae45edd6b8 +begin + mb = pred_raw["mode_boundaries"] + function render_mode(name) + haskey(mb, name) || return md"_(not present)_" + m = mb[name] + kind = get(m, "kind", "?") + oblig = get(m, "obligation", "?") + Tmax = get(m, "T_max_seconds", nothing) + Tmin = get(m, "T_min_seconds", nothing) + time_md = if Tmax === nothing + "_(equilibrium mode — no time bound)_" + else + tmax_str = "$(round(Tmax / 60; digits=1)) min ($(Tmax) s)" + tmin_str = Tmin === nothing ? "_unconstrained_" : "$(round(Tmin / 60; digits=1)) min ($(Tmin) s)" + "T_min: $(tmin_str) · T_max: $(tmax_str)" + end + x_entry = if haskey(m, "X_entry_polytope") && isa(m["X_entry_polytope"], AbstractDict) + ranges = [] + for (k, v) in m["X_entry_polytope"] + isa(v, Vector) && length(v) == 2 || continue + push!(ranges, " - `$k`: [$(v[1]), $(v[2])]") + end + join(ranges, "\n") + else + "_(non-polytope or referenced — see JSON)_" + end + x_safe = get(m, "X_safe_predicate", "?") + x_exit = get(m, "X_exit_predicate", "?") + Markdown.parse(""" + **`$name`** ($(kind)) + + $oblig + + **X_entry:** + $x_entry + + **X_safe:** `$x_safe` + + **X_exit:** `$x_exit` + + **Time:** $time_md + """) + end + render_mode("q_shutdown") +end + +# ╔═╡ dc8758ad-904c-4917-9fba-9a3e42e05e34 +render_mode("q_heatup") + +# ╔═╡ 60bd9d1d-9a04-48e3-a3c9-a84b8bc91009 +render_mode("q_operation") + +# ╔═╡ 561c3d22-4d11-4511-90b7-63b77829454b +render_mode("q_scram") + +# ╔═╡ f50515e2-b205-45ed-acc9-9790697345f8 +md""" +## 7 · Visualization — `t_avg_in_range` × `n_high_trip` projection + +A 2D slice through state space showing the operational deadband on `T_c` +(blue band) inside the high-flux trip on `n` (red ceiling). The intersection +is the comfortable operating polytope — where reach tubes should live. +""" + +# ╔═╡ 015fa1f4-9813-4ede-ad42-8b4f2340bbb8 +begin + T_c0 = 308.349 + Tc_lo = T_c0 - 2.778 + Tc_hi = T_c0 + 2.778 + n_high = 1.15 + n_low = 0.15 + p = plot(xlabel="T_avg [°C]", ylabel="n", + xlim=(280, 322), ylim=(-0.1, 1.4), + title="Operating polytope (intersection of t_avg_in_range × n bounds)", + size=(700, 450), legend=:topleft) + # Operating box + plot!(p, [Tc_lo, Tc_hi, Tc_hi, Tc_lo, Tc_lo], + [n_low, n_low, n_high, n_high, n_low], + linewidth=2, color=:green, label="t_avg_in_range × n bounds") + # Trip lines + hline!(p, [n_high], ls=:dash, color=:red, label="n_high_trip = 1.15") + hline!(p, [n_low], ls=:dash, color=:red, label="n_low_operation = 0.15") + vline!(p, [Tc_lo, Tc_hi], ls=:dot, color=:blue, label="t_avg_in_range ± 2.78 °C") + scatter!(p, [T_c0], [1.0], color=:black, markersize=8, label="x_op (operating point)") +end + +# ╔═╡ 210a3da2-6a5d-48b2-a48e-d87132d5a32f +md""" +## 8 · Edit panel (UX preview — does not persist) + +This panel shows what live editing would look like. **Sliders below do not +write back to `predicates.json`** in v1. Use it to feel out the workflow; +file an issue if a key knob is missing. +""" + +# ╔═╡ 3770e247-c2bd-41a1-9470-0f145f73a894 +@bind ui_t_avg_halfwidth Slider(0.5:0.25:8.0, default=2.78, show_value=true) + +# ╔═╡ 8c67770b-58f8-4868-a3e2-53620565ab5d +@bind ui_n_high_trip Slider(1.05:0.01:1.30, default=1.15, show_value=true) + +# ╔═╡ f88f6809-ad3e-4696-bb12-ad8c30d66a9a +@bind ui_t_standby_offset_F Slider(-90.0:5.0:-30.0, default=-60.0, show_value=true) + +# ╔═╡ b7fdf92d-948b-41f2-8516-dd8fc20c2efe +md""" +**Sketched changes (preview only):** + +- `t_avg_in_range_halfwidth`: $(ui_t_avg_halfwidth) °C (current JSON: 2.778) +- `n_high_trip`: $(ui_n_high_trip) (current JSON: 1.15) +- `T_standby` offset from T_c0: $(ui_t_standby_offset_F) °F (current JSON: -60.0) + +To apply, edit `../reachability/predicates.json` directly. (Write access +will land in app v2.) +""" + +# ╔═╡ 0560c66a-c12f-4f15-bc49-2c9c8164abd1 +md""" +## 9 · Reach traceability + +Which reach artifact has covered which mode invariant? Manual map for now — +later versions will pull this from the latest reach-result `.mat` files. +""" + +# ╔═╡ 1f6abf31-3618-46a5-9f57-4cb3c8022f89 +md""" +| Mode | Invariant | Reach status | Artifact | +|---|---|---|---| +| `q_operation` | `inv2_holds` | ✅ all 6 halfspaces pass (linear, approximate) | `code/scripts/reach_operation.jl` | +| `q_operation` | `inv2_holds` | ❌ Lyapunov barrier fails all 6 (anisotropy) | `code/scripts/barrier_lyapunov.jl` | +| `q_heatup` | `inv1_holds` | ⚠️ TMJets nonlinear works to 10s only (stiffness) | `code/scripts/reach_heatup_nonlinear.jl` | +| `q_heatup` | `inv1_holds` | ❌ no linear reach (time-varying ref needs LTV) | — | +| `q_scram` | (TBD) | ❌ not started | — | +| `q_shutdown` | (TBD) | ❌ not started (trivial — constant u) | — | +""" + +# ╔═╡ de922a70-b653-4b2c-bb13-ccc14b14ac91 +md""" +## 10 · Notes for the next pass + +- v2 should add **write-back** to `predicates.json` (slider → JSON). +- v3: **derive** halfspace concretizations directly from the FRET spec + + a structured vocabulary of physical bounds. The dream FRET-extension + feature. +- Hooks into the latest reach-result MAT files, parsed and shown + per-halfspace. +- 2D projection chooser (currently fixed to T_c × n). +- Mode-transition graph rendered live from `mode_boundaries`. + +--- + +*"Looks ordinary on the surface but is something else underneath."* 🦎 +""" + +# ╔═╡ Cell order: +# ╠═9d14e486-1faa-45a9-b235-6367a039f9da +# ╟─08e80248-89fe-4639-b55c-f10d96de6c31 +# ╟─d7cadb58-e7c4-4701-8fcb-380f1e948d42 +# ╠═c995a73a-c07e-415b-abe8-57abaf9f4b46 +# ╟─48f4bec1-ac48-4318-ba6e-92dbf80a7b2d +# ╟─7ec2cd9d-5c5c-47d7-aa3c-189091b97204 +# ╟─e99c4c2b-7d29-49a4-a474-047f204e331f +# ╟─408432c8-2cc6-4505-8623-9f5614a72c4d +# ╠═0ef6cd25-7f9c-4d64-afdb-ffe8af1ac967 +# ╟─68b1c7bf-c498-41a9-a435-1332c8154035 +# ╠═06be0c87-2a28-4ab3-9fa1-ccde3a9b70d9 +# ╠═8a24ff1e-0afb-4707-89d7-fa50e3b74dbd +# ╟─e67f3259-ce97-4bf5-9e63-8f3aef7c6c56 +# ╠═a17586e3-b8f5-4608-950b-69ae45edd6b8 +# ╠═dc8758ad-904c-4917-9fba-9a3e42e05e34 +# ╠═60bd9d1d-9a04-48e3-a3c9-a84b8bc91009 +# ╠═561c3d22-4d11-4511-90b7-63b77829454b +# ╟─f50515e2-b205-45ed-acc9-9790697345f8 +# ╠═015fa1f4-9813-4ede-ad42-8b4f2340bbb8 +# ╟─210a3da2-6a5d-48b2-a48e-d87132d5a32f +# ╟─3770e247-c2bd-41a1-9470-0f145f73a894 +# ╟─8c67770b-58f8-4868-a3e2-53620565ab5d +# ╟─f88f6809-ad3e-4696-bb12-ad8c30d66a9a +# ╟─b7fdf92d-948b-41f2-8516-dd8fc20c2efe +# ╟─0560c66a-c12f-4f15-bc49-2c9c8164abd1 +# ╟─1f6abf31-3618-46a5-9f57-4cb3c8022f89 +# ╟─de922a70-b653-4b2c-bb13-ccc14b14ac91