ExMaude.IoT (ExMaude v0.4.0)

IoT rule conflict detection using a Maude equational model.

This module evaluates IoT automation rules with the bundled Maude model. Its four checks are inspired by conflict categories in the AutoIoT paper (arxiv.org/abs/2411.10665):

Conflict Types

State Conflict - Two rules target the same device property with incompatible values. Example: motion sensor turns light on while time-based rule turns it off.
Environment Conflict - Two rules produce opposing environmental effects. Example: one rule opens a window to cool, another closes it to reduce noise.
State Cascade - A rule's output triggers another rule, creating unexpected chains. Example: door open → light on → play sound → light off creates oscillation.
State-Environment Cascade - Combined state and environment effects cascade through multiple rules. Example: AC on → window closes → CO2 rises → window opens → conflicts with AC.

Usage

# Define 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
  }
]

# Detect conflicts (the bundled iot-rules.maude module is loaded
# automatically on first call)
{:ok, conflicts} = ExMaude.IoT.detect_conflicts(rules)
# => [%{type: :state_conflict, rule1: "motion-light", rule2: "night-light", ...}]

Telemetry

This module emits the following telemetry events:

[:ex_maude, :iot, :detect_conflicts, :start] - Emitted when detection begins
[:ex_maude, :iot, :detect_conflicts, :stop] - Emitted when detection completes

Measurements include :duration in native time units, :rule_count, and :conflict_count. Metadata includes :result (:ok or :error) and :template (:iot_rules).

See ExMaude.Telemetry for full event documentation and integration examples.

Summary

Types

action()

conflict()

conflict_type()

rule()

state_pred()

A predicate over a world state: a device property holding a value, or an environment key holding a value.

thing_id()

trigger()

world_opts()

Options for the state-space verification functions.

Functions

detect_cascade_conflicts(rules, opts \\ [])

Detects cascade conflicts (both state and state-environment).

detect_conflicts(rules, opts \\ [])

Detects all conflicts in a set of IoT rules.

detect_env_conflicts(rules, opts \\ [])

Detects only environment conflicts in a set of rules.

detect_state_conflicts(rules, opts \\ [])

Detects only state conflicts in a set of rules.

validate_rule(rule)

Validates a rule structure without sending it to Maude.

validate_rules(rules)

Validates a list of rules.

verify_liveness(rules, goal_state, opts \\ [])

Bounded liveness check: looks for a deadlock that prevents rules from reaching goal_state.

verify_safety(rules, bad_state, opts \\ [])

Searches a bounded execution prefix for a world matching bad_state.

Types

action()

@type action() ::
  {:set_prop, thing_id(), String.t(), term()}
  | {:set_env, String.t(), term()}
  | {:invoke, thing_id(), String.t()}

conflict()

@type conflict() :: %{
  type: conflict_type(),
  rule1: String.t(),
  rule2: String.t(),
  reason: String.t()
}

conflict_type()

@type conflict_type() ::
  :state_conflict | :env_conflict | :state_cascade | :state_env_cascade

rule()

@type rule() :: %{
  :id => String.t(),
  :thing_id => thing_id(),
  :trigger => trigger(),
  :actions => [action()],
  optional(:priority) => non_neg_integer()
}

state_pred()

@type state_pred() ::
  {:thing_state, thing_id(), String.t(), term()}
  | {:env_state, String.t(), term()}

A predicate over a world state: a device property holding a value, or an environment key holding a value.

thing_id()

@type thing_id() :: String.t()

trigger()

@type trigger() ::
  {:prop_eq, String.t(), term()}
  | {:prop_gt, String.t(), number()}
  | {:prop_lt, String.t(), number()}
  | {:prop_gte, String.t(), number()}
  | {:prop_lte, String.t(), number()}
  | {:env_eq, String.t(), term()}
  | {:env_gt, String.t(), number()}
  | {:env_lt, String.t(), number()}
  | {:always}
  | {:and, trigger(), trigger()}
  | {:or, trigger(), trigger()}
  | {:not, trigger()}

world_opts()

@type world_opts() :: [
  initial_state: [state_pred()],
  max_depth: pos_integer(),
  timeout: timeout(),
  pool: atom()
]

Options for the state-space verification functions.

:initial_state - bindings present before any rule fires (default [])
:max_depth - bound on search depth (default 50); unbounded searches that hit the bound return {:ok, :unverified} rather than blocking
:timeout - per-search timeout in ms (default 30_000)
:pool - registered caller-owned pool (default :ex_maude_pool)

Functions

detect_cascade_conflicts(rules, opts \\ [])

@spec detect_cascade_conflicts(
  [rule()],
  keyword()
) :: {:ok, [conflict()]} | {:error, term()}

Detects cascade conflicts (both state and state-environment).

Cascade conflicts occur when one rule's output triggers another rule.

detect_conflicts(rules, opts \\ [])

@spec detect_conflicts(
  [rule()],
  keyword()
) :: {:ok, [conflict()]} | {:error, term()}

Detects all conflicts in a set of IoT rules.

Evaluates the given rules against all four checks in the bundled Maude model. Returns a list of detected conflicts, or an empty list if none of those checks match.

Examples

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: _}] = conflicts

Options

:timeout - Maximum time in milliseconds (default: 10000)
:conflict_types - List of conflict types to check (default: all)
:pool - Registered caller-owned pool (default: :ex_maude_pool)

detect_env_conflicts(rules, opts \\ [])

@spec detect_env_conflicts(
  [rule()],
  keyword()
) :: {:ok, [conflict()]} | {:error, term()}

Detects only environment conflicts in a set of rules.

Environment conflicts occur when two rules produce opposing environmental effects.

detect_state_conflicts(rules, opts \\ [])

@spec detect_state_conflicts(
  [rule()],
  keyword()
) :: {:ok, [conflict()]} | {:error, term()}

Detects only state conflicts in a set of rules.

State conflicts occur when two rules target the same device property with incompatible values.

Examples

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

validate_rule(rule)

@spec validate_rule(rule()) :: :ok | {:error, [String.t()]}

Validates a rule structure without sending it to Maude.

Returns :ok if the rule is valid, or {:error, errors} with a list of validation error messages.

Examples

:ok = ExMaude.IoT.validate_rule(%{
  id: "my-rule",
  thing_id: "device-1",
  trigger: {:prop_eq, "state", true},
  actions: [{:set_prop, "device-1", "power", "on"}]
})

{:error, ["missing required field: id"]} = ExMaude.IoT.validate_rule(%{})

validate_rules(rules)

@spec validate_rules([rule()]) ::
  :ok | {:error, %{required(String.t()) => [String.t()]}}

Validates a list of rules.

Returns :ok if all rules are valid, or {:error, errors} with a map of rule IDs to their validation errors.

verify_liveness(rules, goal_state, opts \\ [])

@spec verify_liveness([rule()], state_pred(), world_opts()) ::
  {:ok, :unverified} | {:error, :deadlock_possible | ExMaude.Error.t() | term()}

Bounded liveness check: looks for a deadlock that prevents rules from reaching goal_state.

Searches for a terminal world (=>!, no rule can fire) in which goal_state does not hold. Because the search only inspects terminal states, this detects deadlocks (the system stops short of the goal); it does not detect livelocks (infinite progress that never reaches the goal), which need full LTL model checking.

Returns:

{:error, :deadlock_possible} - a reachable terminal world misses the goal
{:ok, :unverified} - no counterexample was found within the bound, or Maude was unavailable/timed out. This is not an unbounded liveness proof.
{:error, %ExMaude.Error{}} - the verification itself failed (invalid rule encoding, missing module, ...)

Examples

ExMaude.IoT.verify_liveness(rules, {:thing_state, "door", "state", "notified"})
#=> {:ok, :unverified}

verify_safety(rules, bad_state, opts \\ [])

@spec verify_safety([rule()], state_pred() | [state_pred()], world_opts()) ::
  {:ok, :unverified}
  | {:error, {:counterexample, [map()]} | ExMaude.Error.t() | term()}

Searches a bounded execution prefix for a world matching bad_state.

Explores the rule-firing transition system (the IOT-EXEC Maude module) from the initial state with =>* reachability search, looking for a reachable world whose state contains bad_state.

Returns:

{:error, {:counterexample, solutions}} - a reachable bad world (the solutions carry the matching state/substitution)
{:ok, :unverified} - no counterexample was found within the bound, or Maude was unavailable/timed out. A bounded prefix is not a safety proof.
{:error, %ExMaude.Error{}} - the verification itself failed (e.g. a rule that doesn't encode to valid Maude, or a missing module); surfaced as an error rather than :unverified because it indicates a bug in the input, not an inconclusive search

bad_state is a state_pred or a list of them (a list means "all present in the same reachable world").

Examples

# Rule drives a door into an error state when motion is detected.
rules = [%{id: "r1", thing_id: "door", trigger: {:prop_eq, "motion", true},
           actions: [{:set_prop, "door", "state", "error"}], priority: 1}]

ExMaude.IoT.verify_safety(rules, {:thing_state, "door", "state", "error"},
  initial_state: [{:thing_state, "door", "motion", true}])
#=> {:error, {:counterexample, [_ | _]}}