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.
Summary
Functions
The canonical encoding of a state: the smallest of its encodings under every permutation.
Every permutation a symmetry: declaration induces, as substitutions.
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.
What a reduced and an unreduced run must agree on.
Compare the two runs, raising with what differed.
Types
Functions
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.
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.
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.
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.
Compare the two runs, raising with what differed.