# `ExTLA.PropertyTest`
[🔗](https://github.com/dcoai/extla/blob/v0.6.0/lib/ex_tla/property_test.ex#L1)

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
    end

## `stream_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.

# `action_sequences`

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
`c: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`.

# `init_states`

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.

---

*Consult [api-reference.md](api-reference.md) for complete listing*