ExMaude.IoT.ConflictParser (ExMaude v0.2.0)

View Source

Parses Maude conflict detection output into Elixir structures.

This module handles extracting conflict information from Maude's output format, including balanced parenthesis parsing for nested conflict expressions.

Overview

After Maude processes a conflict detection command, it returns output in a specific format. This module parses that output into structured Elixir maps.

Maude Output Format

Maude returns conflict information in this format:

result ConflictSet: noConflict

result ConflictSet: conflict(stateConflict,
  rule("motion-light", ...),
  rule("night-mode", ...),
  "Both rules modify the same property with different values")

Multiple conflicts are separated by |:

conflict(...) | conflict(...) | conflict(...)

Conflict Types

The parser recognizes four conflict types from the AutoIoT paper:

Maude TypeElixir AtomDescription
stateConflict:state_conflictSame device, incompatible states
envConflict:env_conflictOpposing environmental effects
stateCascade:state_cascadeRule output triggers conflicting rule
stateEnvCascade:state_env_cascadeCombined cascading effects

Parsed Output

Each conflict is parsed into a map:

%{
  type: :state_conflict,
  rule1: "motion-light",
  rule2: "night-mode",
  reason: "Both rules modify the same property with different values"
}

Parsing Algorithm

The parser uses balanced parenthesis tracking to handle nested expressions:

  1. Locate conflict( markers in the output
  2. Track parenthesis depth to find matching close paren
  3. Extract conflict type, rule IDs, and reason from each conflict
  4. Deduplicate results (Maude may report same conflict multiple ways)

Edge Cases

  • Returns empty list [] for noConflict output
  • Returns empty list for output without conflict( markers
  • Skips malformed conflict expressions that can't be parsed
  • Handles whitespace and newlines in Maude output

Usage

This module is used internally by ExMaude.IoT.detect_conflicts/2:

# Internal usage
conflicts = ExMaude.IoT.ConflictParser.parse_conflicts(maude_output)
# => [%{type: :state_conflict, rule1: "r1", rule2: "r2", reason: "..."}]

See Also

Summary

Types

conflict()
conflict_type()

Functions

parse_conflicts(output)

Parses Maude output to extract conflict information.

Types

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

Functions

parse_conflicts(output)

@spec parse_conflicts(String.t()) :: [conflict()]

Parses Maude output to extract conflict information.

Returns an empty list if no conflicts are found, or a list of conflict maps.

Examples

output = "result ConflictSet: noConflict"
[] = parse_conflicts(output)

output = "result ConflictSet: conflict(stateConflict, rule(\"r1\"...), rule(\"r2\"...), \"reason\")"
[%{type: :state_conflict, rule1: "r1", rule2: "r2", reason: "reason"}] = parse_conflicts(output)