The compiled representation of a ExTLA.Spec module.
This is what the model checker operates on.
Every function in here is closed over nothing but its arguments, and every one
takes the constant assignments as its first argument. An action's guard and
transition are pure functions of (constants, pre_state, params), and each
param generator is a pure function of (constants, pre_state, params bound so far) — the property that makes successor generation, symmetry canonicalization
and Layer 3's refinement check all straightforward (02-dsl-semantics.md §3).
Why constants are an argument
Every block may reference ^constants (02-dsl-semantics.md §1.1) — the worked
example's conservation_of_money compares against ^max_balance — so guards,
transitions and predicates need them as much as init_fn and the param
generators do. Passing constants uniformly keeps them out of the state, where
they would be fingerprinted and would inflate the state space by a value that
never changes.
Summary
Functions
The action with the given name, or nil.
The declared constant names, in declaration order.
The constant assignments declared with default:, for a run that was given
none of its own.
Extract the compiled spec from a module.
The constant assignments for a run, from application config over the declared defaults.
The instances of a temporal property: \A x \in C : F(x) expanded into one unquantified
formula per element, with the bound values riding along so a finding can say which.
The declared variable names, in declaration order.
Types
@type action_def() :: %{ name: atom(), params: [{atom(), (constants(), ExTLA.State.t(), map() -> Enumerable.t())}], param_sources: [{atom(), param_source()}], guard: (constants(), ExTLA.State.t(), params :: map() -> boolean()), transition: (constants(), ExTLA.State.t(), params :: map() -> ExTLA.State.t()) }
@type action_property_def() :: %{ name: atom(), description: String.t(), predicate: (constants(), old :: ExTLA.State.t(), new :: ExTLA.State.t() -> boolean()) }
@type constants() :: map()
@type init_fn() :: (constants() -> ExTLA.State.t())
@type param_source() :: :constant | :literal | :state
@type predicate() :: (constants(), ExTLA.State.t() -> boolean())
@type state_predicate() :: (ExTLA.State.t() -> boolean())
@type t() :: %ExTLA.Spec.Compiled{ action_properties: [action_property_def()], actions: [action_def()], constants: [constant_def()], fairness: [fairness_def()], init: [init_fn()], invariants: [invariant_def()], module: module(), temporals: [temporal_def()], terminals: [terminal_def()], variables: [variable_def()] }
@type temporal_def() :: %{ name: atom(), description: String.t(), formula: (constants() -> temporal_formula()), opts: keyword() }
@type temporal_formula() :: {:always, temporal_formula()} | {:eventually, temporal_formula()} | {:leads_to, state_predicate(), state_predicate()} | {:predicate, state_predicate()} | {:for_all, (constants() -> Enumerable.t()), (term() -> temporal_formula())}
@type type_expr() :: Macro.t()
Functions
The action with the given name, or nil.
The declared constant names, in declaration order.
The constant assignments declared with default:, for a run that was given
none of its own.
Extract the compiled spec from a module.
Raises ArgumentError for a module that is not a spec, rather than letting an
UndefinedFunctionError surface from three frames down.
The constant assignments for a run, from application config over the declared defaults.
{:error, missing} names the constants nothing assigned, rather than letting a run
proceed on a spec with holes in it. Both mix extla.check and Layer 3's conformance
checking resolve constants HERE rather than each their own way: a specification model
checked with one assignment and an implementation checked against another are two
different specifications, and a verdict from each is not a verdict about the same thing.
A configured key the spec does not declare raises rather than being merged and
ignored. Merged, constants: %{maxx: 100} against constant :max, default: 3 would
resolve to %{max: 3, maxx: 100}: the override the author wrote would be dropped, the
run would use the default, and nothing would say so. It is a raise and not a second
{:error, _} shape because a missing assignment is a legitimate state of a spec (one
meant to be configured per run), while a key naming nothing is a defect in the
configuration, and every caller should refuse it the same way.
@spec temporal_instances(map(), constants()) :: [ %{name: atom(), bound: [term()], formula: temporal_formula()} ]
The instances of a temporal property: \A x \in C : F(x) expanded into one unquantified
formula per element, with the bound values riding along so a finding can say which.
bound is outermost-first — [x, y] for Enum.all?(^xs, fn x -> Enum.all?(^ys, fn y -> …
— and [] for a property with no quantifier.
The one expansion, for both consumers. The liveness checker and ExTLA.Coverage's vacuity
probes both take the instance set from here, so they always agree on what an instance is. A
separate derivation that, say, kept only the innermost binding would land a nested
quantifier's outer instances on one key, and an outer instance whose antecedent never held
would be reported by nothing while the checker checked it.
The declared variable names, in declaration order.