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

A state is an immutable snapshot of all specification variables.
A step is a pair of consecutive states (pre-state and post-state).
A behavior is a (possibly infinite) sequence of states.

A state is a plain map, deliberately: it is the value the DSL's transitions
build and the value `ExTLA.Fingerprint` hashes, and wrapping it in a struct would
buy nothing but an extra field in every fingerprint.

## Missing variables raise

`get/2`, `unchanged?/2` and `prime/3` all fail loudly on a variable the state
does not have. This is not defensiveness; it is the difference between a bug
and a wrong answer. A misspelled variable read through `Map.get/2` returns
`nil`, `nil` compares unequal to whatever the guard expected, the action looks
disabled, and the checker explores a smaller state space and reports success.
Nothing in the output distinguishes that run from a sound one — the same
failure mode, a success reported over states never visited, that
`ExTLA.Fingerprint` prevents at the level below.

# `behavior`

```elixir
@type behavior() :: [t(), ...]
```

# `step`

```elixir
@type step() :: {pre :: t(), post :: t()}
```

# `t`

```elixir
@type t() :: %{required(variable_name()) => value()}
```

# `value`

```elixir
@type value() :: term()
```

# `variable_name`

```elixir
@type variable_name() :: atom()
```

# `changed_vars`

Return the set of variables that changed between states.

    iex> ExTLA.State.changed_vars({%{x: 0, y: 1}, %{x: 2, y: 1}})
    MapSet.new([:x])

# `get`

Return the value of a variable in the given state.

Raises `KeyError` if the variable is not in the state — see the note on
missing variables in the module documentation.

    iex> ExTLA.State.get(%{x: 0}, :x)
    0

# `new`

Create a new state from a keyword list or map of variable assignments.

    iex> ExTLA.State.new(x: 0, y: 1)
    %{x: 0, y: 1}

# `prime`

Return a new state with the given variable updated.
Analogous to TLA+ primed variable assignment: `x' = value`.

Raises `KeyError` if the variable is not already in the state. A TLA+ spec's
variable set is fixed by its `Init`, so priming a variable that is not in the
state is a typo, and a typo that silently widens the state is one the
fingerprint would then faithfully preserve.

    iex> ExTLA.State.prime(%{x: 0, y: 1}, :x, 2)
    %{x: 2, y: 1}

# `prime_many`

Return a new state with multiple variables updated.

    iex> ExTLA.State.prime_many(%{x: 0, y: 1}, %{x: 2, y: 3})
    %{x: 2, y: 3}

# `stuttering?`

Check if two states are identical (stuttering step).

    iex> ExTLA.State.stuttering?({%{x: 0}, %{x: 0}})
    true

# `unchanged?`

Assert that specified variables did NOT change between states.
Analogous to TLA+ `UNCHANGED <<x, y, z>>`.

    iex> ExTLA.State.unchanged?({%{x: 0, y: 1}, %{x: 2, y: 1}}, [:y])
    true

# `validate!`

Assert that every value in the state is deterministically serializable,
per `02-dsl-semantics.md` §6.

Returns the state, so it can be threaded into a pipeline. Raises
`ExTLA.State.InvalidTermError` naming the variable and the position inside it.

Pids, references and ports have no stable identity across runs, and funs
serialize their defining module's version. Floats are excluded for a subtler
reason: `0.0` and `-0.0` compare equal under `==` but encode differently, so
two states that a spec author would call equal would be explored twice — and
`:nan` never equals itself, so a state containing one is not even equal to
itself.

    iex> ExTLA.State.validate!(%{x: 0, q: [:a, {1, "b"}]})
    %{x: 0, q: [:a, {1, "b"}]}

---

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