After recently witnessing yet another instance of a set being mistakenly declared as symmetric when it is actually not, I would like to propose that users be reminded of their responsibility to ensure that a set is indeed symmetry (https://learntla.com/topics/optimization.html#use-symmetry-sets). Additionally, symmetry reduction should not be on while liveness checking.
After recently witnessing yet another instance of a set being mistakenly declared as symmetric when it is actually not, I would like to propose that users be reminded of their responsibility to ensure that a set is indeed symmetry (https://learntla.com/topics/optimization.html#use-symmetry-sets). Additionally, symmetry reduction should not be on while liveness checking.
https://tla.msr-inria.inria.fr/tlatoolbox/doc/model/model-values.html