ExMaude Cheatsheet

Reduce (equations only)

{:ok, "6"} = ExMaude.reduce("NAT", "1 + 2 + 3")
{:ok, "false"} = ExMaude.reduce("BOOL", "true and false")

# Partial functions answer at the kind level
{:ok, "1 / 0"} = ExMaude.reduce("RAT", "1 / 0")

Options: timeout: 5_000

Rewrite (equations + rules)

{:ok, state} = ExMaude.rewrite("MY-MOD", "init")
{:ok, state} = ExMaude.rewrite("MY-MOD", "init", max_rewrites: 100)

Rules can be non-deterministic and may not terminate — always pass a :timeout for unbounded systems.

Search the state space

{:ok, solutions} =
  ExMaude.search("MY-MOD", "init", "goal",
    arrow: "=>*",        # =>1 | =>+ | =>* | =>!
    max_solutions: 5,
    max_depth: 50,
    condition: "isOk(S:State)",   # such that ...
    timeout: 30_000
  )

# Each solution:
# %{solution: 1, state_num: 5, substitution: %{"S:State" => "goal"}}

Search arrows

Loading Maude code

# From a file — loads into every pool worker
:ok = ExMaude.load_file("/path/to/my-module.maude")

# From a string
:ok = ExMaude.load_module("fmod MY-MOD is sort Foo . endfm")

# Preload at worker start (survives worker restarts)
config :ex_maude, preload_modules: ["/path/to/my-module.maude"]

Inspecting

{:ok, "3.5.1"} = ExMaude.version()          # runs maude --version
{:ok, src} = ExMaude.show_module("NAT")
{:ok, listing} = ExMaude.list_modules()
{:ok, parsed} = ExMaude.parse("NAT", "1 + 2")  # parse without reducing

Raw commands

{:ok, output} = ExMaude.execute("show sorts NAT .")

A trailing . is appended automatically when missing.

Keys

config :ex_maude,
  backend: :port,        # :port | :cnode | :nif
  maude_path: nil,       # nil = bundled binary, then system PATH
  pool_size: 4,
  pool_max_overflow: 2,
  timeout: 5_000,        # default command timeout (ms)
  start_pool: false,     # start workers with the application
  use_pty: false,        # Port backend: PTY wrapper opt-in
  preload_modules: []

Backends

All three run Maude as a separate OS process — a Maude crash never takes down the BEAM.

Timeout semantics

IoT rules

rules = [
  %{id: "r1", thing_id: "light-1",
    trigger: {:prop_eq, "motion", true},
    actions: [{:set_prop, "light-1", "state", "on"}],
    priority: 1},
  %{id: "r2", thing_id: "light-1",
    trigger: {:prop_gt, "time", 2300},
    actions: [{:set_prop, "light-1", "state", "off"}],
    priority: 1}
]

{:ok, conflicts} = ExMaude.IoT.detect_conflicts(rules)
# [%{type: :state_conflict, rule1: "r1", rule2: "r2", reason: _}]

Types: :state_conflict, :env_conflict, :state_cascade, :state_env_cascade. Validate first with ExMaude.IoT.validate_rules/1.

Bounded verification

# Safety: is a bad world reachable?
{:ok, :safe} | {:ok, :unverified} |
{:error, {:counterexample, sols}} | {:error, err} =
  ExMaude.IoT.verify_safety(rules,
    {:thing_state, "door", "state", "error"},
    initial_state: [{:thing_state, "door", "motion", true}],
    max_depth: 50, timeout: 30_000)

# Liveness: does every terminal world reach the goal?
{:ok, :live} | {:error, :deadlock_possible} | {:ok, :unverified} =
  ExMaude.IoT.verify_liveness(rules,
    {:thing_state, "door", "state", "notified"})

{:ok, :unverified} = Maude unavailable or timed out (no proof either way). Encoding/module errors surface as {:error, _}.

AI agent policies

{:ok, conflicts} = ExMaude.AI.detect_conflicts(ai_rules)

Extends the IoT vocabulary with capabilities, budgets (intervals), jurisdictions, authority levels, and approval gates.

Telemetry events

[:ex_maude, :command,  :start | :stop | :exception]
[:ex_maude, :server,   :start | :command_start |
                       :command_complete | :timeout | :crash]
[:ex_maude, :pool,     :checkout, :start | :stop]
[:ex_maude, :iot,      :detect_conflicts, :start | :stop]
[:ex_maude, :ai,       :detect_conflicts, :start | :stop]

A :server :timeout event means that worker stopped and the pool is starting a replacement (expect a follow-up :server :start).

Errors

{:error, %ExMaude.Error{type: type, message: msg}} = result
# type ∈ :timeout | :busy | :maude_crash | :parse_error |
#        :module_not_found | :syntax_error | :pool_error | ...
ExMaude.Error.recoverable?(err)  # true for :timeout, :maude_crash

Installing Maude

mix maude.install            # latest release from maude-lang/Maude
mix maude.install 3.5.1      # pin a version

Or point :maude_path at a system installation.