Reduce interchangeable identities only when the property permits it

A permutation of worker identities must preserve permitted initial states and the transition relation. The checked property must also be invariant under that renaming. If every worker follows identical rules and only the number of active workers matters, swapping two opaque identities can preserve the problem. If the algorithm chooses the numerically smallest identifier, assigns one worker a special role, or uses an identity-specific resource limit, unrestricted permutations need not preserve behavior. The relevant symmetry group may then be smaller or trivial, and must be justified explicitly.

Relations among workers also matter. Renaming must consistently transform message endpoints, ownership maps, and other identity-bearing fields, rather than changing one local status array in isolation. A ring topology permits certain rotations but not every arbitrary permutation. Workers in different zones are not interchangeable if the fault model distinguishes zone failures. A property saying that worker A eventually responds is different from a permutation-invariant count property. An apparent similarity in one state variable cannot establish the conditions for reducing the whole specification.

For n identical workers with q local states and no other state, the raw valuation count is q to the power n. Under unrestricted permutations, a class can be described by how many workers occupy each local state. The number of such histograms is the combinations-with-repetition count. For binary local states it is simply n+1, indexed by active-worker count. This is a clean illustrative quotient, not a claim that every service can be represented only by counts; messages, ownership, and shared data can retain many more distinctions.

Do not estimate the reduced count by blindly dividing by n factorial. Some states are unchanged by many permutations: all-inactive and all-active states each form a singleton orbit, while intermediate counts have larger orbits. Distinguishing one worker changes the quotient too. With four binary workers and one fixed identity A, A has two possible states and the other three workers have four possible active counts, giving eight classes instead of five. If a safety assertion mentions A specially, collapsing all four identities would erase a relevant observation.

TLC's model-value symmetry facility relies on the author declaring a genuine symmetry. Its official Toolbox guidance warns that an incorrect declaration can hide errors and says not to use symmetry sets for liveness checking. Treat that as a tool-specific limitation, rather than assuming a safety reduction automatically preserves fairness or identity-dependent progress. Record the symmetry declaration and justify it alongside the property. A successful reduced run should be accompanied by smaller unreduced comparisons and deliberate asymmetric cases where appropriate, while recognizing that such tests do not prove the reduction sound in general.

The reliability instrument shows a count-only observation. Reset, set replica count n=4 and unavailable count k=1, predict three available and majority threshold three, then Play or Step. Separately Reset, set n=4 and k=2, predict two available and the same threshold three, then Play or Step. The model names no replica identities or zones, so different unavailable subsets of equal size share its readout by construction. It cannot establish that those subsets are equivalent for a real protocol, a distinguished leader, a correlated fault model, or a liveness property.