app: Pluto.jl predicate explorer v1 (read-only)

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) <noreply@anthropic.com>
2026-04-20 21:48:08 -04:00 · 2026-04-20 21:48:08 -04:00 · 44cc193829
commit 44cc193829
parent fbbaebff9f
4 changed files with 436 additions and 0 deletions
--- a/app/.gitignore
+++ b/app/.gitignore
@ -0,0 +1 @@
+Manifest.toml
--- a/app/Project.toml
+++ b/app/Project.toml
@ -0,0 +1,10 @@
+authors = ["Dane Sabo <yourstruly@danesabo.com>"]
+
+[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"
--- a/app/README.md
+++ 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.
--- a/app/predicate_explorer.jl
+++ 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