ExMaude Advanced Usage

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]
  ]
)

Loading Custom Modules

ExMaude can load custom Maude modules from files or strings.

Loading from File

# Load the bundled IoT rules module
ExMaude.load_file(ExMaude.iot_rules_path())

Loading from String

# Define a simple counter module
counter_module = """
mod COUNTER is
  protecting NAT .

  sort Counter .
  op counter : Nat -> Counter [ctor] .
  op inc : Counter -> Counter .
  op dec : Counter -> Counter .
  op value : Counter -> Nat .

  var N : Nat .

  eq inc(counter(N)) = counter(s(N)) .
  eq dec(counter(0)) = counter(0) .
  eq dec(counter(s(N))) = counter(N) .
  eq value(counter(N)) = N .
endm
"""

ExMaude.load_module(counter_module)

# Use the custom module
ExMaude.reduce("COUNTER", "value(inc(inc(counter(0))))")

ExMaude.reduce("COUNTER", "value(dec(counter(5)))")

IoT Conflict Detection

ExMaude includes a powerful IoT rule conflict detection system based on formal verification techniques from the AutoIoT paper.

Conflict Types

1. State Conflict - Two rules target the same device with incompatible values
2. Environment Conflict - Two rules produce opposing environmental effects
3. State Cascade - A rule’s output triggers another rule unexpectedly
4. State-Environment Cascade - Combined effects cascade through rules

Example: Detecting State Conflicts

# First, load the IoT rules module
ExMaude.load_file(ExMaude.iot_rules_path())

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

ExMaude.IoT.detect_conflicts(rules)

Complex Rule Definitions

# Rules with compound triggers
complex_rules = [
  %{
    id: "smart-ac",
    thing_id: "ac-1",
    trigger: {:and, {:prop_gt, "temperature", 25}, {:prop_eq, "presence", true}},
    actions: [{:set_prop, "ac-1", "state", "on"}, {:set_env, "temperature", 22}],
    priority: 2
  },
  %{
    id: "window-vent",
    thing_id: "window-1",
    trigger: {:prop_gt, "co2", 800},
    actions: [{:set_prop, "window-1", "state", "open"}],
    priority: 1
  },
  %{
    id: "ac-saver",
    thing_id: "ac-1",
    trigger: {:prop_eq, "window-open", true},
    actions: [{:set_prop, "ac-1", "state", "off"}],
    priority: 3
  }
]

ExMaude.IoT.detect_conflicts(complex_rules)

Pool Management

ExMaude uses a pool of Maude processes for concurrent operations.

Pool Status

ExMaude.Pool.status()

Concurrent Operations

# Run multiple operations concurrently
tasks =
  for i <- 1..5 do
    Task.async(fn ->
      ExMaude.reduce("NAT", "#{i} * #{i}")
    end)
  end

Task.await_many(tasks)

Telemetry

ExMaude emits telemetry events for monitoring and observability.

Available Events

ExMaude.Telemetry.events()

Attaching a Handler

# Simple logging handler
handler = fn event, measurements, metadata, _config ->
  IO.puts("Event: #{inspect(event)}")
  IO.puts("  Duration: #{measurements[:duration]} native units")
  IO.puts("  Metadata: #{inspect(metadata)}")
end

:telemetry.attach(
  "demo-handler",
  [:ex_maude, :command, :stop],
  handler,
  nil
)

# This will trigger the telemetry event
ExMaude.reduce("NAT", "100 + 200")

# Clean up
:telemetry.detach("demo-handler")

Raw Command Execution

For full control, execute raw Maude commands:

# Show module information
ExMaude.execute("show module NAT .")

# List all loaded modules
ExMaude.execute("show modules .")

# Execute multiple commands
commands = """
reduce in NAT : 1 + 1 .
reduce in NAT : 2 * 3 .
reduce in INT : -5 + 10 .
"""

ExMaude.execute(commands)

Next Steps

• Quick Start - Basic operations
• Term Rewriting - Deep dive into rewriting and search
• Benchmarks - Performance metrics