Symmetry Reduction - Revision history

David Geleßus: Update PDF links

2021-02-04T17:15:18Z

Update PDF links

← Older revision		Revision as of 17:15, 4 February 2021
Line 61:		Line 61:

	* "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, [https://www3.hhu.de/stups/downloads/pdf/LeBuSpTu07_209.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>. 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).		* "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>. This is typically the most efficient method.		* "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, [https://www3.hhu.de/stups/downloads/pdf/LeMa07_212.pdf]</ref>. This is typically the most efficient method.

	=References=		=References=
	<references />		<references />

Michael Leuschel: /* Static Symmetry Reduction */

2018-01-12T09:35:55Z

Static Symmetry Reduction

← Older revision		Revision as of 09:35, 12 January 2018
Line 48:		Line 48:
	PROPERTIES D = A \/ B & A /\ B = {} & card(D)=6 & card(A) = 3		PROPERTIES D = A \/ B & A /\ B = {} & card(D)=6 & card(A) = 3
	END		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 ==		== Symmetry Reduction during Model Checking ==

Michael Leuschel: /* Static Symmetry Reduction */

2018-01-12T09:10:03Z

Static Symmetry Reduction

← Older revision		Revision as of 09:10, 12 January 2018
Line 42:		Line 42:
	the free deferred set elements D5,D6,... will be allocated in order to A and 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 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

	== Symmetry Reduction during Model Checking ==		== Symmetry Reduction during Model Checking ==

Michael Leuschel: /* Static Symmetry Reduction */

2018-01-12T08:47:16Z

Static Symmetry Reduction

← Older revision		Revision as of 08:47, 12 January 2018
Line 34:		Line 34:
	a b D3 b		a b D3 b
	a b D3 D3		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.

	== Symmetry Reduction during Model Checking ==		== Symmetry Reduction during Model Checking ==

Michael Leuschel: /* Static Symmetry Reduction */

2015-01-15T16:03:47Z

Static Symmetry Reduction

← Older revision		Revision as of 16:03, 15 January 2015
Line 13:		Line 13:

	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).		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 (666*6 = 1296 solutions, if we ignore the constraint <tt>a /=b</tt>). Luckily, symmetry reduction will reduce this to 10 possibilities.		Thus, in the example above we could have 1080 solutions (666*6 = 1296 solutions, if we ignore the constraint <tt>a/=b</tt>). 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 a first phase ProB will detect, for every deferred set D, a maximal set ds of type D which are disjoint.

Michael Leuschel: /* Static Symmetry Reduction */

2015-01-15T16:03:34Z

Static Symmetry Reduction

← Older revision		Revision as of 16:03, 15 January 2015
Line 13:		Line 13:

	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).		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 666*6 = 1296 solutions, if we ignore the constraint <tt>a /=b</tt>. Luckily, symmetry reduction will reduce this to 10 possibilities.		Thus, in the example above we could have 1080 solutions (666*6 = 1296 solutions, if we ignore the constraint <tt>a /=b</tt>). 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 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 <tt>{a,b}</tt>. These elements will be fixed, in the sense that they will get the numbers 1..k, where k is the size of ds.		In the example above, such a set ds is <tt>{a,b}</tt>. 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).		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.		As of version 1.5, ProB will also further restrict the possible numbers of the remaining constants.

Michael Leuschel: /* Static Symmetry Reduction */

2015-01-15T15:54:56Z

Static Symmetry Reduction

← Older revision		Revision as of 15:54, 15 January 2015
Line 23:		Line 23:

	a b c d		a b c d
	--------------		--------------------------
	a b a a		a b a a
	a b a b		a b a b

Michael Leuschel: /* Static Symmetry Reduction */

2015-01-15T15:54:24Z

Static Symmetry Reduction

← Older revision		Revision as of 15:54, 15 January 2015
Line 20:		Line 20:

	As of version 1.5, ProB will also further restrict the possible numbers of the remaining constants.		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 ([http://www.cs.miami.edu/~geoff/Conferences/CADE/Archive/CADE-19/WS4/04.pdf 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:		It is an adapted technique described in Section 6 of the article "<em>New Techniques that Improve MACE-style Finite Model Finding</em>" ([http://www.cs.miami.edu/~geoff/Conferences/CADE/Archive/CADE-19/WS4/04.pdf 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 c d

Michael Leuschel at 15:53, 15 January 2015

2015-01-15T15:53:48Z

← Older revision		Revision as of 15:53, 15 January 2015
Line 13:		Line 13:

	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).		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 666*6 = 1296 solutions, if we ignore the constraint <~~pre~~>a /=b</~~pre~~>. Luckily, symmetry reduction will reduce this to 10 possibilities.		Thus, in the example above we could have 666*6 = 1296 solutions, if we ignore the constraint <tt>a /=b</tt>. 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 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 <~~pre~~>{a,b}</~~pre~~>. These elements will be fixed, in the sense that they will get the numbers 1..k, where k is the size of ds.		In the example above, such a set ds is <tt>{a,b}</tt>. 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).		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).

			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 ([http://www.cs.miami.edu/~geoff/Conferences/CADE/Archive/CADE-19/WS4/04.pdf 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

	== Symmetry Reduction during Model Checking ==		== 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).		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).

Michael Leuschel at 15:44, 15 January 2015

2015-01-15T15:44:45Z

@@ Line 2: / Line 2: @@
 [[Category:Stubs]]
 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).