Define a named action (state transition).

params: is the action's only source of nondeterminism. Inside the block, require expr is an enabling condition, let pat = expr is an ordinary local binding, and variable = expr is a next-state equation whose right-hand side reads the pre-state. Variables not assigned are implicitly UNCHANGED.

See 02-dsl-semantics.md §2-3 for the full semantics.

Define an action property (transition constraint).

The block is a bare boolean expression; old and new are implicitly bound. A bare variable name is a compile error here — see 02-dsl-semantics.md §4.

Declare a constant parameter. Its value is assigned at model-check time. Referenced in blocks as ^name.

Options

• default: — the assignment mix extla.check uses when nothing else supplies one. A checker cannot start without a value for every constant, and a default beside the declaration supplies one without a second file. Application config still overrides it, and ExTLA.ModelChecker.run/2 ignores it entirely.

Declare fairness constraints (02-dsl-semantics.md §5.2).

fairness :weak, [:done, :reset]        # WF(Done), WF(Reset)
fairness :strong, acquire_lock: [:p]   # \A p : SF(AcquireLock(p))

Whole-action fairness guarantees only that some binding fires, which is consistent with one process starving while the others take turns — so any per-process property needs the second form.

Naming an action that does not exist, params that are not a leading prefix of the action's params, or a state-drawn param, is a compile error. Those checks run in @before_compile, where every action is known regardless of declaration order.

Define an initial state. Variables are assigned with =; every declared variable must be assigned exactly once.

Multiple init blocks are disjuncted — a nondeterministic choice of starting state.

Define a state invariant (safety property), checked in every reachable state.

The block is a bare boolean expression over variables and ^constants. desc: carries a description; it is an option rather than a positional string because two trailing optional positionals cannot be told apart.

Define a temporal property (liveness), within the bounded fragment of 02-dsl-semantics.md §5.1. A formula outside the fragment is a compile error naming the unsupported operator — never a silently weaker check.

Declare a legitimate end state (02-dsl-semantics.md §5.3). A successor-less state satisfying any terminal predicate is not reported as a deadlock.

Nothing else changes: invariants are still checked there, no action is disabled by it, and for liveness it stutters forever.

Declare a state variable with an optional type: annotation. Referenced in blocks as a bare name.

The type is stored quoted and resolved at model-check time, because nearly every useful type mentions a constant (02-dsl-semantics.md §1.5). It is checked as the implicit invariant :type_ok in every reachable state; it does NOT restrict exploration, so a state outside its type is a reported violation rather than a pruned branch.