ExMaude (ExMaude v0.3.0)

Elixir bindings for the Maude formal specification and verification system.

ExMaude provides a high-level API for interacting with Maude, a formal specification language based on rewriting logic. It supports:

Term reduction and normalization
Module loading and management
Search operations for state space exploration
IoT rule conflict detection (ExMaude.IoT)
AI rule conflict detection (ExMaude.AI)
Pluggable backend architecture (Port, C-Node, NIF)

Quick Start

# Start the application (automatic with supervision tree)
{:ok, _} = Application.ensure_all_started(:ex_maude)

# Reduce a term
{:ok, result} = ExMaude.reduce("NAT", "1 + 2 + 3")
# => {:ok, "6"}

# Load a custom module
:ok = ExMaude.load_file("/path/to/my-module.maude")

# Search for states
{:ok, states} = ExMaude.search("MY-MOD", "initial", "final", max_depth: 10)

Configuration

config :ex_maude,
  backend: :port,                # :port | :cnode | :nif
  maude_path: nil,               # nil = auto-detect bundled binary
  pool_size: 4,                  # Worker processes
  pool_max_overflow: 2,          # Extra workers under load
  timeout: 5_000,                # Default command timeout
  start_pool: false,             # Auto-start on application boot
  use_pty: false                 # PTY wrapper opt-in (Port backend only)

Architecture

ExMaude uses a pluggable backend architecture with a Poolboy worker pool. Each worker maintains a persistent Maude session.

                      ExMaude (Public API)
                            │
                  ExMaude.Backend (Behaviour)
                            │
      ┌─────────────────────┼─────────────────────┐
      │                     │                     │
      ▼                     ▼                     ▼
Backend.Port         Backend.CNode         Backend.NIF
      │                     │                     │
      ▼                     ▼                     ▼
 Pipes + Maude CLI   Erlang Distribution   Rust-managed Maude
                     + C bridge process    subprocess (pipes)

Backends

All three backends run Maude as a separate OS process — a Maude crash never takes down the BEAM. They differ in transport and in how much native code runs inside the BEAM itself:

Backend	Transport	Latency	Use Case
`:port`	Erlang Port over pipes	Higher	Default, pure Elixir, works everywhere
`:cnode`	Erlang distribution to a C bridge	Medium	Structured binary protocol; needs epmd and the compiled bridge
`:nif`	Rustler NIF driving the subprocess	Lowest	Hot paths; the Rust layer runs inside the BEAM (panics are caught, a segfault would crash the VM)

Summary

Functions

ai_rules_path()

Returns the path to the bundled AI rules Maude module.

execute(command, opts \\ [])

Executes a raw Maude command and returns the output.

iot_rules_path()

Returns the path to the bundled IoT rules Maude module.

list_modules(opts \\ [])

Lists all loaded modules.

load_file(path)

Loads a Maude file into all pool workers.

load_module(source)

Loads a Maude module from a string.

parse(module, term, opts \\ [])

Parses a term in the given module without reducing it.

reduce(module, term, opts \\ [])

Reduces a term in the given module to its normal form.

rewrite(module, term, opts \\ [])

Rewrites a term using the rules in the given module.

search(module, initial, pattern, opts \\ [])

Searches for states reachable from an initial term.

show_module(module, opts \\ [])

Shows the definition of a loaded module.

version()

Returns the Maude interpreter version.

Functions

ai_rules_path()

@spec ai_rules_path() :: Path.t()

Returns the path to the bundled AI rules Maude module.

AI rules extend the IoT rules vocabulary with capability ontology, tool-invocation arguments, budget arithmetic via interval reasoning, sovereignty constraints, authority levels, and approval gates. Used by ExMaude.AI for verifying AI-generated automation rules and multi-tenant agent policies.

execute(command, opts \\ [])

@spec execute(
  String.t(),
  keyword()
) :: {:ok, String.t()} | {:error, term()}

Executes a raw Maude command and returns the output.

Use this for commands not covered by the high-level API.

Examples

ExMaude.execute("show module NAT .")
#=> {:ok, "fmod NAT is ..."}

iot_rules_path()

@spec iot_rules_path() :: Path.t()

Returns the path to the bundled IoT rules Maude module.

list_modules(opts \\ [])

@spec list_modules(keyword()) :: {:ok, String.t()} | {:error, term()}

Lists all loaded modules.

Examples

{:ok, modules} = ExMaude.list_modules()

load_file(path)

@spec load_file(Path.t()) :: :ok | {:error, ExMaude.Error.t()}

Loads a Maude file into all pool workers.

Examples

ExMaude.load_file("/path/to/my-module.maude")
#=> :ok

load_module(source)

@spec load_module(String.t()) :: :ok | {:error, ExMaude.Error.t()}

Loads a Maude module from a string.

Examples

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

parse(module, term, opts \\ [])

@spec parse(String.t(), String.t(), keyword()) :: {:ok, String.t()} | {:error, term()}

Parses a term in the given module without reducing it.

Useful for checking syntax and seeing how Maude disambiguates a term.

Examples

ExMaude.parse("NAT", "1 + 2 + 3")
#=> {:ok, "1 + 2 + 3"}

Options

:timeout - Maximum time in milliseconds (default: 5000)

reduce(module, term, opts \\ [])

@spec reduce(String.t(), String.t(), keyword()) ::
  {:ok, String.t()} | {:error, term()}

Reduces a term in the given module to its normal form.

Examples

ExMaude.reduce("NAT", "1 + 2")
#=> {:ok, "3"}

ExMaude.reduce("STRING", ""hello" + " " + "world"")
#=> {:ok, ""hello world""}

Options

:timeout - Maximum time in milliseconds (default: 5000)

rewrite(module, term, opts \\ [])

@spec rewrite(String.t(), String.t(), keyword()) ::
  {:ok, String.t()} | {:error, term()}

Rewrites a term using the rules in the given module.

Unlike reduce/3, this applies rewrite rules (potentially non-deterministically) rather than just equations.

Examples

ExMaude.rewrite("MY-MOD", "initial-state", max_rewrites: 100)
#=> {:ok, "final-state"}

search(module, initial, pattern, opts \\ [])

@spec search(String.t(), String.t(), String.t(), keyword()) ::
  {:ok, [map()]} | {:error, term()}

Searches for states reachable from an initial term.

Uses Maude's search command to explore the state space defined by rewrite rules.

Examples

ExMaude.search("MY-MOD", "init", "target", max_depth: 10)
#=> {:ok, [%{solution: 1, state_num: 5, substitution: %{"S" => "target"}}]}

Options

:max_depth - Maximum search depth (default: 100)
:max_solutions - Maximum solutions to find (default: 1)
:arrow - Search arrow: =>1 (one step), =>+ (one or more), =>* (zero or more), =>! (terminal states only) (default: =>*)
:condition - Additional search condition (such that ...)
:timeout - Maximum time in milliseconds (default: 30000)

show_module(module, opts \\ [])

@spec show_module(
  String.t(),
  keyword()
) :: {:ok, String.t()} | {:error, term()}

Shows the definition of a loaded module.

Examples

ExMaude.show_module("NAT")
#=> {:ok, "fmod NAT is ..."}

version()

@spec version() :: {:ok, String.t()} | {:error, term()}

Returns the Maude interpreter version.

Runs maude --version on the resolved binary; works without a started pool.

Examples

ExMaude.version()
#=> {:ok, "3.5.1"}