Powered by AppSignal & Oban Pro

Scenario 3 — The verifier is not a yes-man

priv/livebooks/03_clean_rules.livemd

Scenario 3 — The verifier is not a yes-man

unless Code.ensure_loaded?(Goatmire.Verifier) do
  repo = System.get_env("LIVEBOOK_GOATMIRE_DIR") || Path.expand("../..", __DIR__)
  unless File.regular?(Path.join(repo, "mix.exs")) do
    raise "Open this notebook from a full Goatmire clone, or set LIVEBOOK_GOATMIRE_DIR to that clone. See notebooks/README.md."
  end
  maude = System.get_env("MAUDE_PATH") || System.find_executable("maude") ||
    Path.join(repo, "deps/ex_maude/priv/maude/bin/maude")
  unless File.regular?(maude) do
    raise "Install Maude in the clone with mix deps.get and mix maude.install --version 3.5.1, or set MAUDE_PATH."
  end
  Mix.start()
  Mix.env(:prod)
  Mix.install(
    [{:goatmire, path: repo, env: :prod}],
    config: [ex_maude: [maude_path: maude]],
    config_path: :goatmire,
    lockfile: :goatmire,
    start_applications: false
  )
  Application.put_all_env(goatmire: [role: :notebook, transport: Goatmire.Transport.Local,
    metrics_enabled: false, vda5050_enabled: false, autostart_fleet: false,
    real_devices: [], modbus_sensors: []])
  {:ok, _} = Application.ensure_all_started(:goatmire)
end

What this notebook is for

A conflict detector that flags everything is a conflict detector nobody keeps. The clean set exists to prove the gate can say nothing is wrong, and to be precise about what that sentence covers.

Goatmire.Verifier.health()

Five unrelated rules

Five Things, five properties. No rule writes a property another rule triggers on, and no two rules share a Thing.

rules = Goatmire.Rules.clean_set()
Enum.map(rules, &{&1.id, &1.thing_id})
{:ok, verdict} = Goatmire.Verifier.verify(rules)
{verdict.status, verdict.conflicts, verdict.duration_us}

Say what that means, and only that

verdict.scope

None of the four conflict types encoded in the bundled model matched. That is a narrower statement than "these rules are safe", and the narrow one is the one worth making — a tool that claims more than it checked is trusted right up until the moment it matters.

Now break it on purpose

Add a sixth rule that writes a property one of the five triggers on, and the cascade check has something to find.

cascading = rules ++ [
  %{
    id: "beacon-drives-torque-alarm",
    thing_id: "conveyor-3",
    trigger: {:prop_eq, "beacon", "amber"},
    actions: [{:set_prop, "conveyor-3", "torque_nm", 200}],
    priority: 1
  }
]

{:ok, broken} = Goatmire.Verifier.verify(cascading)
{broken.status, Enum.map(broken.conflicts, & &1[:type])}

A model dependency example

Five rules reuse the property name state. The detector sees dependency edges; the runtime reads each rule’s own Thing, so this corpus does not demonstrate an executable cross-device cycle. It also omits temperature feedback from HVAC-off. Read the witness as a model interaction.

{:ok, %{verdict: cascade_verdict}} = Goatmire.ScenarioRunner.cascade_example()
{cascade_verdict.status, Enum.map(cascade_verdict.conflicts, &{&1[:type], &1[:rule1], &1[:rule2]})}

This is the shape a pairwise eyeball review misses, because every individual pair looks reasonable and the problem is in the composition.