Random messages, derived from a spec's own action definitions.
The spec's params: are where nondeterminism lives (02-dsl-semantics.md §3), so they
are also the domain of possible messages: pick an action, pick a binding of its params
from the generators the action declares, and ask the refinement for the concrete message
that causes it.
Why the refinement is an argument
A specification has no notion of a message — that is the whole reason
ExTLA.Refinement.concrete_message/2 exists — so a generator returning one needs the
mapping as well. The alternative, returning {action, params} and mapping later, would
put half the generator in its caller; ExTLA.PropertyTest.action_sequences/3 is that
spec-level form, for a consumer's own property tests.
Summary
Functions
A generator restricted to actions whose guard holds in the current state.
A generator over every action, enabled or not.
Functions
A generator restricted to actions whose guard holds in the current state.
Cheaper per step, and the right choice when the question is "does the implementation
follow the spec where the spec has something to say" rather than "does it refuse what
the spec forbids". A simulation that only ever sends enabled messages cannot produce a
:not_enabled finding, which is worth knowing before choosing it.
A generator over every action, enabled or not.
Returns (abstract_state -> {action, params, message}) | nil, nil when nothing can be
generated in that state. Messages for disabled actions are the point rather than waste:
an implementation that accepts a message the spec forbids in that state is exactly what
ExTLA.GenServer.Runtime.check_step!/5 reports as :not_enabled, and a generator that never sends one can
never find it.