ExTLA.Spec (ExTLA v0.6.0)

Copy Markdown View Source

use ExTLA.Spec turns a module into a specification.

defmodule Specs.Counter do
  use ExTLA.Spec

  constant :max
  variable :n, type: 0..^max

  init do
    n = 0
  end

  action :increment do
    require n < ^max
    n = n + 1
  end

  invariant :within_bounds do
    n >= 0 and n <= ^max
  end
end

The declarations accumulate into module attributes and compile to ordinary functions on the module; @before_compile assembles them into a ExTLA.Spec.Compiled struct, reachable as Specs.Counter.__tla_spec__/0 or ExTLA.Spec.Compiled.from_module/1.

The DSL's semantics are normative in 02-dsl-semantics.md, and every rule there is enforced when this module compiles — a spec either means something precise or does not compile.