StreamData generators derived from a specification, for a consumer's own property tests.
They are the piece of Layer 3 that ExTLA does not drive: ExTLA.Replay checks an implementation against a
trace and ExTLA.Simulation walks it randomly, both under ExTLA's control, while these
hand the spec's own state space to a check all the consumer writes.
property "the server conforms under any initial state" do
check all state <- ExTLA.PropertyTest.init_states(Specs.TransferProtocol, constants) do
...
end
endstream_data is not a dependency of ExTLA, and these still work
It is declared only: [:dev, :test], so nothing in lib/ may reference StreamData
unconditionally. Each function below is compiled behind Code.ensure_loaded?(StreamData)
— the shape ExTLA.Invariant.Test already uses — with an else clause that says so
rather than failing as an undefined function. A consumer who wants generators declares
stream_data themselves; ExTLA keeps zero runtime dependencies.
No generated test files
ExTLA does not write test modules for you. Generated test code is code someone then has to maintain; these property helpers give most of the value without that.
Summary
Functions
A generator over the spec's behaviours, as {action, params} steps.
A generator over the spec's initial states.
Functions
A generator over the spec's behaviours, as {action, params} steps.
Every generated sequence is a real behaviour: it starts at one of the spec's initial states, and at every step the action it names is enabled with the binding it names. Nothing generated is a sequence the spec forbids.
Where the choices come from
ExTLA.ModelChecker.enabled_steps/3 — the checker's own enumeration. A second
implementation of "what may happen next" could disagree with the checker, and then a
generated behaviour would not be one the checker explored.
Why there is no refinement argument
ExTLA.Simulation.Generator takes one and returns a concrete message; this returns
{action_name, params} and stops there. A sequence of actions is spec-level, and
mapping it to messages is the consumer's own check all body, which calls
ExTLA.Refinement.concrete_message/2 itself. The two signatures differ on purpose.
Shrinking
Sound, and for a structural reason: every prefix of a behaviour is a behaviour, so a shorter sequence from the same initial state is still one the spec admits. The length is generated first and shrinks toward zero, so a shrunk counterexample is a sequence the implementation really could have taken — a generator that shrank into an invalid sequence would report failures that cannot happen, which is the failure mode worth guarding.
A walk that runs out of enabled actions stops there, so a sequence may be shorter than
the length drawn. It is never longer than max_length.
A generator over the spec's initial states.
Why this is a generator over a finite set
An init block is a function of the constants and nothing else — nondeterminism in
the DSL comes from params: and only from params: (02-dsl-semantics.md §3) — so a
spec with three disjuncted init blocks has exactly three initial states, not a
space to sample. This enumerates them and picks among them.
It is typed as a generator anyway, and that is not a formality: it is what lets an
initial state compose into a check all beside generators that really are large,
and it shrinks toward the first init block, which is the one most specs write as
their base case.
What it refuses
A state outside the permitted state terms (02-dsl-semantics.md §6) raises, and so does one outside the variables'
declared types — both naming the init block and the variable. A spec whose init
produces such a state is one mix extla.check would refute at depth 1, and a generator
that quietly filtered it away would hide the same defect behind a property that
silently tested less than it appeared to.