Symmetry Reduction
Symmetry reduction is a technique used in model checking to reduce the state space of a model by exploiting symmetries in the model.
This works, but the document is not complete.
Sometimes you would want a simple value for the ID or Key.
Instead of defining the keys as strings or numbers,
you can define them as symmetric_values
.
Run in playground


Mark the role as symmetric, and the model checker will automatically mark the symmetric transitions as equivalent.
Run in playground


You can try it by removing the symmetric
keyword
and see the difference in the number of states generated.
To reduce states explored, remember to use bags when possible instead of lists. This will ensure, the order of operations are not relevant. For more information on the available data structures, see the Data structures tutorial.