ProB can make use of symmetries induced by the use of deferred sets in B (and given sets in Z).

Static Symmetry Reduction

ProB will perform a limited form of symmetry reduction for constants which are elements of deferred sets. Take the following example

MACHINE m SETS D
CONSTANTS a,b,c,d
PROPERTIES a:D & b:D & a/=b & c:D & d:D & card(D)=6
END

Elements of a deferred set D of cardinality n are given a number between 1 and n (the pretty printer of ProB renders those elements as D1,...,Dn respectively). Thus, in the example above we could have 1080 solutions (6*6*6*6 = 1296 solutions, if we ignore the constraint a/=b). Luckily, symmetry reduction will reduce this to 10 possibilities.

In a first phase ProB will detect, for every deferred set D, a maximal set ds of type D which are disjoint. In the example above, such a set ds is {a,b}. These elements will be fixed, in the sense that they will get the numbers 1..k, where k is the size of ds. Thus, a will denote D1, b will denote D2. ProB's pretty printer will actually use a instead of D1, and b instead of D2 (and a and b will actually disappear from the list of constants visible in the state properties view). This reduces the number of possibilities already to 36.

As of version 1.5, ProB will also further restrict the possible numbers of the remaining constants. It is an adapted technique described in Section 6 of the article "New Techniques that Improve MACE-style Finite Model Finding" (PDF). Basically, the technique ensures that c will not use the index 4 and that d will use the index 4 only if the index 3 was used by c. Thus only the 10 following possibilities are generated by ProB:

a	b	c	d
--------------------------
a	b	a	a
a	b	a	b
a	b	D3	D4
a	b	a	D3
a	b	b	a
a	b	b	b
a	b	b	D3
a	b	D3	a
a	b	D3	b
a	b	D3	D3

As of version 1.8, ProB will furthermore detect partition constraints for the deferred sets. This symmetry reduction is applied to the free, unconstrained deferred set elements. For the example above, these would be all elements with index 5 or higher (D5, D6, ...). For the example above, if we have a constraint

 D = A \/ B & A /\ B = {}

the free deferred set elements D5,D6,... will be allocated in order to A and B. In other words, we can have D5 in A and D6 in B, but not D6 in A and D5 in B.

In the machine below all deferred set elements are free:

MACHINE m SETS D
CONSTANTS A,B
PROPERTIES D = A \/ B & A /\ B = {} & card(D)=6 & card(A) = 3
END

Hence, here ProB 1.8 will only generate one possible setup of the constants:

A = {D1,D2,D3}
B = {D4,D5,D6}

Symmetry Reduction during Model Checking

In addition to the above, you can also turn of stronger symmetry reduction for model checking.

Warning: turning on symmetry reduction will also influence the way that animation works. In other words, when executing an operation, the animator may transfer you to an equivalent symmetric state (rather than to the one you may have expected).

In the "Symmetry" menu of the "Preferences" menu you can choose the following:

• "off": symmetry reduction is turned off.
• "flood": This performs permutation flooding, whereby all permutations of a newly added state are automatically added (and marked as already treated). This does not reduce the number of states of the state space, but it may still considerably reduce the number of transitions and the number of states which need to be checked (for invariant violations and for computing outgoing transitions). More details: ^[1]
• "nauty": This approach translates a B state into a graph and uses the nauty package in order to compute a canonical form of this graph. If two states have the same canonical form, they are considered equivalent and only one of them is explored ^[2]. Warning: nauty sometimes can take a long time to compute the canonical form for complicated states (and in this case it will not respond to ProB's standard time-out mechanism).
• "hash": This approach computes a symbolic hash value for every state, having the important property that two symmetric states have the same hash value. Note that this is an "approximate" method, as two non-symmetric states may also be mapped to the same hash value^[3]. This is typically the most efficient method.

References