Victoria.Apalache (Victoria v0.1.0)

Copy Markdown View Source

Runs a validated Apalache plan and materializes every generated ITF trace.

Execution is synchronous, supports exactly Apalache v0.58.3, invokes the executable without a shell, and retains the exclusively reserved run directory on success and failure. Victoria imposes no runtime timeout.

Summary

Functions

run(plan, options \\ [])

Executes plan with Apalache v0.58.3.

Functions

run(plan, options \\ [])

@spec run(
  Victoria.Apalache.Plan.t(),
  keyword()
) :: {:ok, Victoria.Apalache.Result.t()} | {:error, Victoria.Apalache.Error.t()}

Executes plan with Apalache v0.58.3.

The only option is :executable. A successful result means at least one top-level regular ITF file was discovered and every discovered trace loaded; Apalache may have returned a nonzero status. Invalid arguments raise ArgumentError.