# ExMaude Cheatsheet

## Core operations
{: .col-2}

### Reduce (equations only)

```elixir
{: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)

```elixir
{: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

```elixir
{: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

| Arrow | Meaning                          |
| ----- | -------------------------------- |
| `=>1` | exactly one rewrite step         |
| `=>+` | one or more steps                |
| `=>*` | zero or more steps (default)     |
| `=>!` | terminal states only (no further rewrites) |

## Modules and raw commands
{: .col-2}

### Loading Maude code

```elixir
# 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

```elixir
{: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

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

A trailing ` .` is appended automatically when missing.

## Configuration
{: .col-2}

### Keys

```elixir
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.

| Backend  | Transport                  | Latency |
| -------- | -------------------------- | ------- |
| `:port`  | Erlang Port over pipes     | higher  |
| `:cnode` | Distribution + C bridge    | medium  |
| `:nif`   | Rustler-managed subprocess | lowest  |

### Timeout semantics

| Timeout | Bounds |
| ------- | ------ |
| command `:timeout` | one Maude command; on expiry the worker **restarts** |
| `Pool.transaction` `:checkout_timeout` | the wait for a free worker |
| `Pool.broadcast` `:timeout` | per-worker budget; keep it ≥ the command timeout |

## Conflict detection
{: .col-2}

### IoT rules

```elixir
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

```elixir
# 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

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

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

## Operations
{: .col-2}

### Telemetry events

```text
[: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

```elixir
{: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

```bash
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.