Compiles an action's params: — the DSL's only source of nondeterminism
(02-dsl-semantics.md §3).
An earlier draft had two mechanisms: params: for constant-drawn values and
choose/1,2 inside the block for state-drawn ones. The second was both
redundant and misnamed — TLA+'s CHOOSE is deterministic Hilbert choice — and
it could not work anyway: a function returning one element cannot produce
several successors.
With one mechanism, an action body is a pure deterministic function of
(pre_state, params). That single property is what makes successor generation,
enabling checks, symmetry canonicalization and Layer 3's refinement check all
straightforward, so any construct that reintroduces in-body branching has to be
rejected for the same reason.
A param may draw from:
| Form | Source | Example |
|---|---|---|
| A constant | :constant | from: ^accounts |
| A literal range or list | :literal | amount: 1..10, mode: [:a, :b] |
| A function of the pre-state | :state | t: fn s -> s.pending end |
Params bind left to right, and a state function may take a second argument receiving the params bound before it — which is how a spec keeps the combinatorial explosion down, filtering in the generator rather than generating every combination and rejecting most of them in the guard.
Summary
Functions
Compile the params: option into generator bodies and their sources.