{{v1, v2}, {v1, v3}, {v2, v3}} is not a tuple, but a set (of sets), and sets are unordered. Therefore, {{v3, v2}, {v3, v1}, {v2, v1}} is the same set as the first one. But note that you cannot even write this set unless you have access to the names of its elements.
A CHOOSE expression allows you to name an element of the set, distinguishing it from the others.
Suppose we have a constant parameter S, instantiated to the set of model values {v1,v2,v3}, and a definition
someS == CHOOSE x \in S : TRUE
Then the expression
IF s = someS THEN 0 ELSE 42
returns 0 for the chosen value but 42 for the others and is therefore not symmetric in S. This shows that S cannot be declared as a symmetry set for a specification that contains these entities.
The other TLA+ operators do not allow you to name elements of your parameter sets, for example you cannot explicitly build the tuple
<< v1, v2, v3 >>
which would not be symmetric in S. In contrast, expressions such as
{ seq \in Seq(S) : Len(seq) = 3 }
i.e., the set of all triples built from S, are symmetric.
In contrast, replacing the definition of someS with the operator definition
notS == CHOOSE x : x \notin S
does not destroy symmetry of the specification with respect to S. In particular, the test
s = notS
returns FALSE for all elements of S.
In summary, symmetry reduction is very helpful for model checking, but deciding if a parameter can be declared as a symmetry set for a given specification can be subtle.
Regards,
Stephan