AGENTS.md

Guidance for AI agents working with ExMaude.

For detailed usage patterns and API guidelines, see usage-rules.md.

Project Overview

ExMaude is an Elixir library providing bindings to Maude formal verification system. It features a pluggable backend architecture with Poolboy worker pool management.

Architecture

                        ExMaude (Public API)
                              │
                    ExMaude.Backend (Behaviour)
                              │
        ┌─────────────────────┼─────────────────────┐
        │                     │                     │
        ▼                     ▼                     ▼
ExMaude.Backend.Port   ExMaude.Backend.CNode   ExMaude.Backend.NIF
        │                     │                     │
        ▼                     ▼                     ▼
   PTY + Maude CLI    Erlang Distribution    Direct libmaude
                      + maude_bridge          via Rustler

Backend Comparison

Module Overview

ExMaude (Main API)
    │
    ├── ExMaude.Backend         Backend behaviour and selection
    │   ├── Backend.Port        PTY-based Port communication
    │   ├── Backend.CNode       Erlang C-Node bridge
    │   └── Backend.NIF         Rustler NIF (lowest latency)
    │
    ├── ExMaude.Binary          Maude binary management & platform detection
    ├── ExMaude.Maude           High-level operations (reduce, rewrite, search)
    ├── ExMaude.Pool            Poolboy worker pool management
    ├── ExMaude.Server          Delegates to Backend.impl()
    ├── ExMaude.Parser          Output parsing utilities
    ├── ExMaude.Telemetry       Telemetry events and helpers
    │
    ├── ExMaude.IoT             IoT rule conflict detection API
    │   ├── IoT.Encoder         Rule-to-Maude encoding
    │   ├── IoT.Validator       Rule validation
    │   └── IoT.ConflictParser  Conflict output parsing
    │
    ├── ExMaude.Term            Structured term representation
    ├── ExMaude.Error           Structured error types
    └── ExMaude.Result.*        Result types (Reduction, Search, Solution)

Key Files

Development Commands

mix setup                       # Install deps
mix test                        # Run tests (unit only)
mix test --include integration  # Run with Maude
mix test --include network      # Run GitHub API tests
mix lint                        # Format + Credo + Dialyzer
mix check                       # All quality checks
mix sobelow                     # Security analysis
mix docs                        # Generate docs
mix maude.install               # Install Maude binary
mix maude.install --check       # Check Maude availability
mix coveralls                   # Test coverage report (text)
mix coveralls.json              # Test coverage report (json/codecov)
mix bench                       # Run main benchmarks
mix bench.backends              # Run backend comparison benchmarks

C-Node Compilation

The C-Node backend requires compilation:

cd c_src && make      # Compile maude_bridge binary
cd c_src && make clean  # Clean build artifacts

Or automatically via elixir_make during mix compile.

Testing

• Unit tests - Run without Maude, test parsing/validation logic
• Integration tests - Tagged @tag :integration, require Maude binary
• Network tests - Tagged @tag :network, make GitHub API calls
• Use ExMaude.MaudeCase for integration test setup

Test structure:

test/
├── ex_maude/
│   ├── maude_test.exs        # Maude module tests
│   ├── pool_test.exs         # Pool tests
│   ├── server_test.exs       # Server tests
│   ├── parser_test.exs       # Parser unit tests
│   ├── telemetry_test.exs    # Telemetry event tests
│   ├── iot_test.exs          # IoT module tests
│   ├── error_test.exs        # Error type tests
│   ├── term_test.exs         # Term type tests
│   └── integration_test.exs  # Full integration tests
├── mix/tasks/                 # Mix task tests
└── support/
    └── maude_case.ex         # Shared integration test setup

Telemetry Events

ExMaude emits standard telemetry events:

See ExMaude.Telemetry.events/0 for programmatic access.

Error Handling

All errors use ExMaude.Error struct with standardized types:

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 app start
  use_pty: true                        # Use PTY wrapper (Port backend)

Backend Selection

# Check available backends
ExMaude.Backend.available_backends()
#=> [:port] or [:port, :cnode]

# Get current backend module
ExMaude.Backend.impl()
#=> ExMaude.Backend.Port

Common Patterns

Running Maude Commands

# High-level API (preferred)
{:ok, result} = ExMaude.reduce("NAT", "1 + 2")
{:ok, solutions} = ExMaude.search("MOD", "init", "goal")

# Low-level with pool
ExMaude.Pool.transaction(fn worker ->
  ExMaude.Server.execute(worker, "reduce in NAT : 1 + 2 .")
end)

Loading Modules

# From file (broadcasts to all workers)
:ok = ExMaude.load_file("/path/to/module.maude")

# From string
:ok = ExMaude.load_module("fmod TEST is ... endfm")

# IoT rules module
:ok = ExMaude.load_file(ExMaude.iot_rules_path())

IoT Conflict Detection

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

{:ok, conflicts} = ExMaude.IoT.detect_conflicts(rules)

Commit Conventions

All commits must follow the Conventional Commits specification. git_ops parses these to auto-generate CHANGELOG.md and determine version bumps.

Format: type(optional scope): description

Do not add Co-Authored-By or any AI/Claude attribution to commit messages.

Release Flow

1. mix git_ops.release — updates changelog, bumps version in mix.exs and README.md, commits, and tags
2. git push --follow-tags — pushes commit and tag
3. CI (publish.yml) triggers on v* tag → runs checks → mix hex.publish

References

• usage-rules.md - Detailed usage patterns
• README.md - Quick start guide
• Maude System
• Maude Manual
• AutoIoT Paper - IoT conflict detection