m ("") |
No edit summary |
||
| Line 9: | Line 9: | ||
* "off": symmetry reduction is turned off. | * "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: <ref>Michael Leuschel, Michael Butler, Corinna Spermann and Edd Turner: Symmetry Reduction for B by Permutation Flooding, Proceedings of the 7th International B Conference (B2007),2007,pp. 79-93,LNCS 4355,Springer, [http://www.stups.uni-duesseldorf.de/publications/poor_mansym_B2007_final.pdf]</ref> | * "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: <ref>Michael Leuschel, Michael Butler, Corinna Spermann and Edd Turner: Symmetry Reduction for B by Permutation Flooding, Proceedings of the 7th International B Conference (B2007),2007,pp. 79-93,LNCS 4355,Springer, [http://www.stups.uni-duesseldorf.de/publications/poor_mansym_B2007_final.pdf]</ref> | ||
* "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 <ref>Corinna Spermann and Michael Leuschel: ProB gets Nauty: Effective Symmetry Reduction for B and Z Models, Proceedings Symposium TASE 2008,June,2008,pp. 15-22,IEEE</ref>. | * "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 <ref>Corinna Spermann and Michael Leuschel: ProB gets Nauty: Effective Symmetry Reduction for B and Z Models, Proceedings Symposium TASE 2008,June,2008,pp. 15-22,IEEE</ref>. 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<ref>Michael Leuschel and Thierry Massart: ProB gets Nauty: Efficient Approximate Verification of B via Symmetry Markers, Proceedings International Symmetry Conference,Januar,2007,Verlag, [http://www.stups.uni-duesseldorf.de/publications/final-symmetry.pdf]</ref>. | * "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<ref>Michael Leuschel and Thierry Massart: ProB gets Nauty: Efficient Approximate Verification of B via Symmetry Markers, Proceedings International Symmetry Conference,Januar,2007,Verlag, [http://www.stups.uni-duesseldorf.de/publications/final-symmetry.pdf]</ref>. This is typically the most efficient method. | ||
=References= | =References= | ||
<references /> | <references /> | ||
ProB can make use of symmetries induced by the use of deferred sets in B (and given sets in Z).
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: