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

Symmetry reduction: states that differ only by a permutation of interchangeable
constants are one state.

`symmetry: [:processes]` says the elements of `^processes` are interchangeable — process
ids, account names, replica ids. For a symmetric set of size *n*, the reachable space
shrinks by up to a factor of *n!*, which is the difference between tractable and not for
exactly the specs this tool is for.

The mechanism is canonical form. Before a state is fingerprinted it is rewritten under
every permutation of every symmetric set and the smallest encoding wins, so two
symmetric states share a fingerprint by construction and the second is never explored.

## What it costs

*n*! encodings per state for one symmetric set of size *n*, and the product for several.
Three processes and two resources is twelve encodings per state to explore up to twelve
times fewer states — a wash at best in wall-clock, a clear win at four or five elements.
It is a lever to be measured on your model, not assumed.

## What it assumes, and who checks it

Symmetry is sound only if nothing in the spec can tell the elements apart: no
`Enum.at(^accounts, 0)`, no `Enum.sort`, no `<` on process names, no dependence on list
position. **Nothing verifies this statically**, and ExTLA does not pretend otherwise: a
constant flows into arbitrary Elixir, so the check is undecidable,
and any conservative approximation rejects the `Enum.all?(^processes, …)` every real
spec is built from. Soundness is the author's obligation, exactly as it is in TLC.

What the tool does instead is make a wrong declaration *detectable*.
`verify_symmetry: true` runs the same model with and without the reduction and fails if
any verdict differs. Counts differ on purpose — that is what the reduction is for — so
it is the verdicts that are compared. Run it once on a small constant assignment before
trusting the reduction on the large one.

# `mapping`

```elixir
@type mapping() :: %{required(term()) =&gt; term()}
```

One permutation, as the substitution it performs on the elements it moves.

# `canonical`

The canonical encoding of a state: the smallest of its encodings under every permutation.

Comparing encodings rather than terms is deliberate. `ExTLA.Fingerprint.canonical/1` is
already the thing state identity is defined by, so the smallest encoding is a canonical
form in exactly the sense the fingerprint cares about — and Erlang's term order, which
compares an integer below an atom, is not.

# `mappings`

Every permutation a `symmetry:` declaration induces, as substitutions.

The identity is among them, so the unpermuted encoding always competes. Elements are
sorted first, so the permutation list — and therefore every fingerprint — is the same on
every run.

# `permute`

A state with every occurrence of a symmetric element replaced, wherever it appears —
as a value, inside a set or a sequence, as a map key, or nested in any of those.

# `verdict`

What a reduced and an unreduced run must agree on.

Not the counts: a sound reduction changes those on purpose, and comparing them would
fail on every declaration that worked. What has to survive the reduction is every answer
the run gives — whether it verified, what it refuted, whether it got stuck, and which
actions it never enabled.

# `verify!`

Compare the two runs, raising with what differed.

---

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