The type: annotation grammar of 02-dsl-semantics.md §1.5.
Type expressions are a small language of their own, distinct from the block
DSL, and they are stored quoted: nearly every useful type mentions a
constant (0..^max_val, [^servers ~> :set]) that has no value when the
module compiles. This module checks the shape at compile time so an
ill-formed type is a diagnostic rather than a crash halfway through a
model-checking run; resolution against the constant assignments happens later,
in the checker, where the implicit :type_ok invariant is evaluated.
| Form | Meaning |
|---|---|
:atom, 0, "s" | Exactly that literal |
[:a, :b] | One of the listed literals |
a..b | An integer in the range; either bound may be ^const, and either may be negative |
a..b//step | Every stepth integer from a up to b — 0..10//2 is 0, 2, …, 10 |
^name | Any element of the constant (which must be a set) |
t1 | t2 | Union — a value of either type |
{t1, t2, …} | A tuple of that arity, element-wise |
[dom ~> rng] | A map whose keys are exactly dom and whose values are in rng |
%{k: t, …} | A record: a map with exactly these keys, each value of its type |
:set, :seq | Any MapSet / any list, elements unconstrained |
set(t), seq(t) | A MapSet / list whose every element is of type t |
:int, :nat | Any integer / any non-negative integer |
Summary
Types
A type expression with its constants substituted, ready to test values against.
Functions
Check a state against the resolved variable types.
Render a resolved type for a violation message.
Explain a :type_ok violation: which variable, what it holds, what it declared.
The implicit :type_ok invariant for a run, or nil when no variable is typed.
Whether a value inhabits a resolved type.
Resolve a stored type expression against the constant assignments.
The typed variables of a spec, resolved against this run's constants.
Check that type is in the §1.5 grammar. Returns the expression unchanged —
it is stored quoted — or raises ExTLA.Spec.CompileError.
Types
@type resolved() :: {:literal, term()} | {:one_of, [term()]} | {:range, integer(), integer()} | {:range, integer(), integer(), integer()} | {:element_of, MapSet.t()} | {:union, [resolved()]} | {:tuple, [resolved()]} | {:function, MapSet.t(), resolved()} | {:record, %{required(term()) => resolved()}} | {:set_of, resolved()} | {:seq_of, resolved()} | :set | :seq | :int | :nat
A type expression with its constants substituted, ready to test values against.
Functions
Check a state against the resolved variable types.
Types are checked as an invariant rather than used to prune, so a state outside its type is a reported violation and not a silently narrower search.
Render a resolved type for a violation message.
Explain a :type_ok violation: which variable, what it holds, what it declared.
The implicit :type_ok invariant for a run, or nil when no variable is typed.
It is checked in every reachable state, which is why a coverage report lists a
type_ok the spec never declared.
Whether a value inhabits a resolved type.
Resolve a stored type expression against the constant assignments.
This happens at model-check time, not at compile time, because nearly every
useful type mentions a constant that has no value until a run assigns
one. where names the variable, for the error message.
The typed variables of a spec, resolved against this run's constants.
Resolution happens once per run rather than once per state: the constants do not change, and the state space is where the work is.
Check that type is in the §1.5 grammar. Returns the expression unchanged —
it is stored quoted — or raises ExTLA.Spec.CompileError.
constants is the set of declared constant names; a ^name naming something
else is reported here rather than at check time.