@spec execute(
  String.t(),
  keyword()
) :: {:ok, String.t()} | {:error, term()}

Executes a raw Maude command.

Use this for commands not covered by the high-level API.

Examples

ExMaude.Maude.execute("show module NAT .")
#=> {:ok, "fmod NAT is ..."}

ExMaude.Maude.execute("parse in NAT : 1 + 2 .")
#=> {:ok, "1 + 2"}

@spec list_modules(keyword()) :: {:ok, String.t()} | {:error, term()}

Lists all loaded modules.

@spec load_file(Path.t()) :: :ok | {:error, ExMaude.Error.t()}

Loads a Maude file into all pool workers.

The file is loaded into every worker in the pool to ensure consistent module availability across all operations.

Examples

ExMaude.Maude.load_file("/path/to/my-module.maude")
#=> :ok

@spec load_module(String.t()) :: :ok | {:error, term()}

Loads a Maude module from a string.

The module definition is loaded into all pool workers.

Examples

source = "fmod MY-MOD is sort Foo . endfm"
ExMaude.Maude.load_module(source)
#=> :ok

@spec parse(String.t(), String.t(), keyword()) :: {:ok, String.t()} | {:error, term()}

Parses a term in the given module without reducing.

Examples

ExMaude.Maude.parse("NAT", "1 + 2 + 3")
#=> {:ok, "1 + (2 + 3)"}

@spec reduce(String.t(), String.t(), keyword()) ::
  {:ok, String.t()} | {:error, term()}

Reduces a term in the given module to its normal form.

Uses Maude's reduce command which applies equations until a normal form is reached (equations are applied as simplification rules).

Examples

ExMaude.Maude.reduce("NAT", "1 + 2 + 3")
#=> {:ok, "6"}

ExMaude.Maude.reduce("BOOL", "true and false")
#=> {:ok, "false"}

Options

• :timeout - Maximum time in ms (default: 5000)

@spec rewrite(String.t(), String.t(), keyword()) ::
  {:ok, String.t()} | {:error, term()}

Rewrites a term using the rules in the given module.

Uses Maude's rewrite command which applies both equations and rules. Rules can be non-deterministic and may not terminate.

Examples

ExMaude.Maude.rewrite("MY-MOD", "initial-state", max_rewrites: 100)
#=> {:ok, "final-state"}

Options

• :max_rewrites - Maximum number of rule applications (default: unlimited)
• :timeout - Maximum time in ms (default: 5000)

@spec search(String.t(), String.t(), String.t(), keyword()) ::
  {:ok, [map()]} | {:error, term()}

Searches for states reachable from an initial term.

Uses Maude's search command to explore the state space defined by rewrite rules. Returns solutions matching the target pattern.

Examples

ExMaude.Maude.search("MY-MOD", "init", "goal")
#=> {:ok, [%{solution: 1, state_num: 5, substitution: %{}}]}

ExMaude.Maude.search("MY-MOD", "init", "S:State", condition: "property(S)")
#=> {:ok, [%{solution: 1, state_num: 3, substitution: %{"S:State" => "s1"}}]}

Options

• :max_depth - Maximum search depth (default: 100)
• :max_solutions - Maximum solutions to find (default: 1)
• :arrow - Search arrow: =>1, =>+, =>*, =>! (default: =>*)
• :condition - Additional search condition
• :timeout - Maximum time in ms (default: 30000)

@spec show_module(
  String.t(),
  keyword()
) :: {:ok, String.t()} | {:error, term()}

Shows information about a module.

Examples

ExMaude.Maude.show_module("NAT")
#=> {:ok, "fmod NAT is ..."}

@spec version() :: {:ok, String.t()} | {:error, term()}

Returns Maude version information.

Examples

ExMaude.Maude.version()
#=> {:ok, "Maude (version available at runtime)"}