ExMaude Quick Start

Mix.install(
  [
    {:ex_maude, path: Path.join(__DIR__, ".."), env: :dev}
  ],
  config_path: :ex_maude,
  lockfile: :ex_maude,
  config: [
    ex_maude: [start_pool: true, use_pty: false]
  ]
)

Introduction

ExMaude is an Elixir client for Maude, a high-performance reflective language and system supporting equational and rewriting logic specification and programming.

Maude excels at:

• Term rewriting - Reducing expressions to normal forms
• Equational reasoning - Working with algebraic specifications
• State space exploration - Model checking and search
• Formal verification - Proving properties about systems

Basic Operations

Reduce

The reduce command evaluates a term to its normal form using equations:

# Simple arithmetic in the NAT (natural numbers) module
ExMaude.reduce("NAT", "1 + 1")

# More complex expression
ExMaude.reduce("NAT", "2 * 3 + 4")

# Working with integers (negative numbers)
ExMaude.reduce("INT", "-5 + 10")

Parse

The parse command checks if a term is valid without evaluating it:

ExMaude.parse("NAT", "1 + 2 * 3")

# Invalid term returns an error
ExMaude.parse("NAT", "invalid syntax here")

Rewrite

The rewrite command applies rewrite rules (which may be non-deterministic):

# Rewrite with a maximum number of rewrites
ExMaude.rewrite("NAT", "s(0) + s(s(0))", max_rewrites: 100)

Working with Strings

Maude has a built-in STRING module:

ExMaude.reduce("STRING", ~s("Hello" + " " + "World"))

ExMaude.reduce("STRING", ~s(length("ExMaude")))

ExMaude.reduce("STRING", ~s(substr("Hello World", 0, 5)))

Error Handling

ExMaude returns {:ok, result} or {:error, reason} tuples:

# Successful operation
case ExMaude.reduce("NAT", "1 + 1") do
  {:ok, result} -> "Result: #{result.term}"
  {:error, error} -> "Error: #{inspect(error)}"
end

# Module not found
ExMaude.reduce("NONEXISTENT-MODULE", "1 + 1")

# Parse error in term
ExMaude.reduce("NAT", "1 + + 1")

Raw Command Execution

For advanced use cases, you can execute raw Maude commands:

ExMaude.execute("reduce in NAT : 10 * 10 .")

ExMaude.execute("show module NAT .")

Checking Maude Version

ExMaude.version()

Pool Status

ExMaude uses a pool of Maude processes for concurrent operations:

ExMaude.Pool.status()

Next Steps

• Advanced Usage - Custom modules, IoT conflict detection, pooling
• Term Rewriting - Deep dive into rewriting and search
• Benchmarks - Performance metrics