Selecto.Verification.BoundedModel (Selecto v0.4.8)

Copy Markdown

Deterministic, exhaustive checking over an explicitly bounded state space.

This is a small model-checking kernel used by Selecto's verification suites. It is deliberately dependency-free so verification is available to package consumers and Mix tasks, not only to the test environment.

A successful report proves that every invariant held for every supplied state. The proof is bounded by the caller's finite model; the report records the exact model size and never presents the result as an unbounded theorem.

Summary

Types

invariant()
report()

Functions

check(model, states, invariants)

Checks every invariant against every state and returns a stable proof report.

Types

invariant()

@type invariant() ::
  {String.t() | atom(), (term() -> :ok | true | {:error, term()} | false)}

report()

@type report() :: %{
  format: String.t(),
  format_version: pos_integer(),
  proof_level: :bounded_exhaustive,
  model: String.t(),
  state_count: non_neg_integer(),
  invariant_count: non_neg_integer(),
  check_count: non_neg_integer(),
  proved?: boolean(),
  counterexamples: [map()]
}

Functions

check(model, states, invariants)

@spec check(String.t() | atom(), Enumerable.t(), [invariant()]) :: report()

Checks every invariant against every state and returns a stable proof report.

Invariants should return :ok or true when satisfied. {:error, reason}, false, exceptions, and throws are captured as reproducible counterexamples.