Graphical Visualization - Revision history

Michael Leuschel at 12:02, 6 January 2024

2024-01-06T12:02:30Z

← Older revision		Revision as of 12:02, 6 January 2024
Line 3:		Line 3:
	The graphical visualization of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables the user to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B variable or expression. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed where. We now show how this animation can be done with very little effort.		The graphical visualization of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables the user to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B variable or expression. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed where. We now show how this animation can be done with very little effort.

	~~Note that~~ ProB ~~now~~ also supports more powerful ~~visualization~~ based on SVG and HTML in the form of [[VisB]].		As an alternative you can also specify [[CUSTOM_GRAPH]] definitions to render the current state as graph laid out by GraphViz.
			In addition, ProB also supports more powerful visualizations based on SVG and HTML in the form of [[VisB]].

	== The Graphical Animation Model ==		== The Graphical Animation Model ==

Michael Leuschel at 11:55, 6 January 2024

2024-01-06T11:55:02Z

← Older revision		Revision as of 11:55, 6 January 2024
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
	The graphical visualization of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables the user to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B ~~specification~~. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed. We now show how this animation can be done with very little effort.		The graphical visualization of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables the user to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B variable or expression. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed where. We now show how this animation can be done with very little effort.

			Note that ProB now also supports more powerful visualization based on SVG and HTML in the form of [[VisB]].

	== The Graphical Animation Model ==		== The Graphical Animation Model ==

Michael Leuschel: /* Sudoku */

2018-10-12T06:41:25Z

Sudoku

← Older revision		Revision as of 06:41, 12 October 2018
Line 194:		Line 194:
	)		)

	=== Other Features		=== Other Features ===

	One can define actions for right clicks and mouse clicks and drags:		One can define actions for right clicks and mouse clicks and drags:

Michael Leuschel: /* Sudoku */

2018-10-12T06:41:05Z

Sudoku

@@ Line 193: / Line 193: @@
                          c:dom(Sudoku9(r)) & i:1.. fullsize & i = Sudoku9(r)(c)}
+                        )
 = References =
 <references/>

Michael Leuschel: /* The Graphical Animation Model */

2014-06-27T06:08:03Z

The Graphical Animation Model

← Older revision		Revision as of 06:08, 27 June 2014
Line 14:		Line 14:
	The function fa is declared by defining ANIMATION_FUNCTION and ideally should be of type INTEGER * INTEGER +-> INTEGER. If the function fa is defined for r and c, then the animator should display the image with number fa(r,c) at row r and column c. If the function is undefined at this position, no image is displayed in the corresponding cell.		The function fa is declared by defining ANIMATION_FUNCTION and ideally should be of type INTEGER * INTEGER +-> INTEGER. If the function fa is defined for r and c, then the animator should display the image with number fa(r,c) at row r and column c. If the function is undefined at this position, no image is displayed in the corresponding cell.

	Notes: ProB will try and convert your expression to INTEGER * INTEGER +-> INTEGER (~~e.g., each enumerated set element will be converted to its position in the SETS clause~~). Instead of an ANIMATION_IMGx one can also declare ANIMATION_STRx definitions for textual representations. If there is no image or string definition for the number fa(r,c) or if fa(r,c) is no number then ProB will try and display the result in pretty-printed textual format.		Notes: ProB will try and convert your expression to INTEGER * INTEGER +-> INTEGER (see below). Instead of an ANIMATION_IMGx one can also declare ANIMATION_STRx definitions for textual representations. If there is no image or string definition for the number fa(r,c) or if fa(r,c) is no number then ProB will try and display the result in pretty-printed textual format.

	The dimension of the grid is computed by examining the minimum and maximum coordinates that occur in the animation function. More precisely,		The dimension of the grid is computed by examining the minimum and maximum coordinates that occur in the animation function. More precisely,

	the rows are in the range min(dom(dom(~~f,,a,,~~)))..max(dom(dom(~~f,,a,,~~))) and		the rows are in the range min(dom(dom(fa)))..max(dom(dom(fa))) and

	the columns are in the range min(ran(dom(~~f,,a,,~~)))..max(ran(dom(~~f,,a,,~~))).		the columns are in the range min(ran(dom(fa)))..max(ran(dom(fa))).

	We take the B machine of the sliding 8-puzzle as an example. In the 8-puzzle, the tiles are numbered. Every tile can be moved horizontally and vertically into an empty square. The final configuration is reached whenever all the tiles are in order.		We take the B machine of the sliding 8-puzzle as an example. In the 8-puzzle, the tiles are numbered. Every tile can be moved horizontally and vertically into an empty square. The final configuration is reached whenever all the tiles are in order.

Michael Leuschel: /* The Graphical Animation Model */

2014-06-27T06:04:46Z

The Graphical Animation Model

← Older revision		Revision as of 06:04, 27 June 2014
Line 10:		Line 10:
	ANIMATION_IMGx == "filename", where x is the number of the image and "filename" is its path to a gif image file.		ANIMATION_IMGx == "filename", where x is the number of the image and "filename" is its path to a gif image file.

	2. A user-defined animation function ~~f,,a,,~~ is evaluated to recompute the graphical output for every state. The graphical output of ~~f,,a,,~~ is known as the graphical visualization, which consists of a two-dimensional grid. Each cell in the grid can contain an image. The function uses the variables r (for row) and c (for column) to determine in which cell the image will be displayed. An image can appear multiple times in the grid.		2. A user-defined animation function fa is evaluated to recompute the graphical output for every state. The graphical output of fa is known as the graphical visualization, which consists of a two-dimensional grid. Each cell in the grid can contain an image. The function uses the variables r (for row) and c (for column) to determine in which cell the image will be displayed. An image can appear multiple times in the grid.

	The function ~~f,,a,,~~ is declared by defining ANIMATION_FUNCTION and ~~must~~ be of type INTEGER * INTEGER +-> INTEGER. If the function ~~f,,a,,~~ is defined for r and c, then the animator should display the image with number ~~f,,a,,~~(r,c) at row r and column c. ~~Otherwise~~, no image is displayed in the corresponding cell.		The function fa is declared by defining ANIMATION_FUNCTION and ideally should be of type INTEGER * INTEGER +-> INTEGER. If the function fa is defined for r and c, then the animator should display the image with number fa(r,c) at row r and column c. If the function is undefined at this position, no image is displayed in the corresponding cell.

			Notes: ProB will try and convert your expression to INTEGER * INTEGER +-> INTEGER (e.g., each enumerated set element will be converted to its position in the SETS clause). Instead of an ANIMATION_IMGx one can also declare ANIMATION_STRx definitions for textual representations. If there is no image or string definition for the number fa(r,c) or if fa(r,c) is no number then ProB will try and display the result in pretty-printed textual format.

	The dimension of the grid is computed by examining the minimum and maximum coordinates that occur in the animation function. More precisely,		The dimension of the grid is computed by examining the minimum and maximum coordinates that occur in the animation function. More precisely,
Line 86:		Line 88:
	ANIMATION_FUNCTION_DEFAULT == DefaultImages;		ANIMATION_FUNCTION_DEFAULT == DefaultImages;
	ANIMATION_FUNCTION == CurrentImages;		ANIMATION_FUNCTION == CurrentImages;

			Note: as of version 1.4 of ProB you can define multiple animation functions (e.g., ANIMATION_FUNCTION1, ANIMATION_FUNCTION2, ...) each overriding its predecessor.

	This was used next in the Sudoku example.		This was used next in the Sudoku example.

Joy Clark: s to z, " " hinzufügen

2011-04-18T11:27:10Z

s to z, " " hinzufügen

← Older revision		Revision as of 11:27, 18 April 2011
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
	The graphical ~~visualisation~~ of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables the user to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B specification. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed. We now show how this animation can be done with very little effort.		The graphical visualization of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables the user to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B specification. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed. We now show how this animation can be done with very little effort.

	== The Graphical Animation Model ==		== The Graphical Animation Model ==
Line 51:		Line 51:
	END		END

	On the left side of the following Figure, the non-graphical ~~visualisation~~ is generated by ProB. It is readable, but the graphical ~~visualisation~~ at the right side is much easier to understand.		On the left side of the following Figure, the non-graphical visualization is generated by ProB. It is readable, but the graphical visualization at the right side is much easier to understand.

	[[File:Puzzle_graphical1.png]]		[[File:Puzzle_graphical1.png]]
Line 137:		Line 137:
	[[File:scheduler_graphvis1.png]]		[[File:scheduler_graphvis1.png]]

	The graphical ~~visualisation~~ is done by writing in the DEFINTIONS section the following animation function. Here, we need to map PID elements to image numbers.		The graphical visualization is done by writing in the DEFINTIONS section the following animation function. Here, we need to map PID elements to image numbers.

	IsPidNrci == p=process1 & i=1) or (p=process2 & i=2) or (p=process3 & i=3));		IsPidNrci == p=process1 & i=1) or (p=process2 & i=2) or (p=process3 & i=3));
Line 178:		Line 178:
	);		);

	The following Figure shows the non-graphical ~~visualisation~~ of a particular puzzle (left), the graphical ~~visualisation~~ of the puzzle (middle), as well as the ~~visualisation~~ of the solution found by ProB after a couple of seconds (right).		The following Figure shows the non-graphical visualization of a particular puzzle (left), the graphical visualization of the puzzle (middle), as well as the visualization of the solution found by ProB after a couple of seconds (right).

	[[File:Sudoku_graphvis1.png]]		[[File:Sudoku_graphvis1.png]]


	Note that it would have been nice to be able to replace Nri inside the animation function simply by i = Sudoku9(r)(c). While our ~~visualisation~~ algorithm can automatically convert set elements to numbers, the problem is that there is a type error in the override: the left-hand side is a function of type INTEGERINTEGER+->INTEGER, while the right-hand side now becomes a function of type INTEGERINTEGER+->NRS. One solution is to write multiple definitions of the animation function. In addition to the standard animation function, we can define a default background animation function. The standard animation function will override the default animation function, but the overriding is done within the graphical animator and not within a B formula. In this way, one can now rewrite the above animation as follows:		Note that it would have been nice to be able to replace Nri inside the animation function simply by i = Sudoku9(r)(c). While our visualization algorithm can automatically convert set elements to numbers, the problem is that there is a type error in the override: the left-hand side is a function of type INTEGERINTEGER+->INTEGER, while the right-hand side now becomes a function of type INTEGERINTEGER+->NRS. One solution is to write multiple definitions of the animation function. In addition to the standard animation function, we can define a default background animation function. The standard animation function will override the default animation function, but the overriding is done within the graphical animator and not within a B formula. In this way, one can now rewrite the above animation as follows:

	ANIMATION_FUNCTION_DEFAULT == ( {r,c,i\|r:1..fullsize & c:1..fullsize & i=0} );		ANIMATION_FUNCTION_DEFAULT == ( {r,c,i\|r:1..fullsize & c:1..fullsize & i=0} );

Joy Clark: /* The Graphical Animation Model */ word choice edited

2011-04-14T11:50:27Z

The Graphical Animation Model: word choice edited

← Older revision		Revision as of 11:50, 14 April 2011
Line 51:		Line 51:
	END		END

	On the left side of the following Figure, the non-graphical visualisation is generated by ProB. It is readable, but the graphical visualisation at the right side is much ~~more inspiring and understandable~~.		On the left side of the following Figure, the non-graphical visualisation is generated by ProB. It is readable, but the graphical visualisation at the right side is much easier to understand.

	[[File:Puzzle_graphical1.png]]		[[File:Puzzle_graphical1.png]]

Joy Clark: grammatical edits, punctuation edits

2011-04-14T09:12:27Z

grammatical edits, punctuation edits

Jens Bendisposto at 14:02, 18 January 2010

2010-01-18T14:02:36Z

← Older revision		Revision as of 14:02, 18 January 2010
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
			__NOTOC__
	The graphical visualisation of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B specification. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed. We now show how this animation can be done with very little effort.		The graphical visualisation of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B specification. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed. We now show how this animation can be done with very little effort.

← Older revision		Revision as of 09:12, 14 April 2011
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	__NOTOC__		__NOTOC__
	The graphical visualisation of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B specification. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed. We now show how this animation can be done with very little effort.		The graphical visualisation of ProB <ref>M. Leuschel, M. Samia, J. Bendisposto and L. Luo: Easy Graphical Animation and Formula Viewing for Teaching B. In C. Attiogbé and H. Habrias, editors, Proceedings: The B Method: from Research to Teaching, pages 17-32, Nantes, France. APCB, 2008.</ref> enables the user to easily write custom graphical state representations in order to provide a better understanding of a model. With this method, one assembles a series of pictures and writes an animation function in B. Each picture can be associated to a specific state of a B specification. Then, depending on the current state of the model, the animation function in B stipulates which pictures should be displayed. We now show how this animation can be done with very little effort.

	== The Graphical Animation Model ==		== The Graphical Animation Model ==
Line 10:		Line 10:
	ANIMATION_IMGx == "filename", where x is the number of the image and "filename" is its path to a gif image file.		ANIMATION_IMGx == "filename", where x is the number of the image and "filename" is its path to a gif image file.

	2. A user-defined animation function f,,a,, is evaluated to recompute the graphical output for every state. The graphical output of f,,a,, is known as the graphical ~~visualisation~~, which consists of a two-dimensional grid ~~and where each~~ cell in the grid can contain an image. ~~Depending on~~ row r and column ~~c, an~~ image is displayed ~~in a cell~~. An image can appear multiple times in the grid.		2. A user-defined animation function f,,a,, is evaluated to recompute the graphical output for every state. The graphical output of f,,a,, is known as the graphical visualization, which consists of a two-dimensional grid. Each cell in the grid can contain an image. The function uses the variables r (for row) and c (for column) to determine in which cell the image will be displayed. An image can appear multiple times in the grid.

	The function f,,a,, is declared by defining ANIMATION_FUNCTION and must be of type INTEGER * INTEGER +-> INTEGER. If the function f,,a,, is defined for r and c, then the animator should display the image with number f,,a,,(r,c) at row r and column c. Otherwise, no image is displayed in the corresponding cell.		The function f,,a,, is declared by defining ANIMATION_FUNCTION and must be of type INTEGER * INTEGER +-> INTEGER. If the function f,,a,, is defined for r and c, then the animator should display the image with number f,,a,,(r,c) at row r and column c. Otherwise, no image is displayed in the corresponding cell.

	The dimension of the grid is computed by ~~looking at~~ the minimum and maximum coordinates that occur in the animation function. More precisely,		The dimension of the grid is computed by examining the minimum and maximum coordinates that occur in the animation function. More precisely,

	the rows are in the range min(dom(dom(f,,a,,)))..max(dom(dom(f,,a,,))) and		the rows are in the range min(dom(dom(f,,a,,)))..max(dom(dom(f,,a,,))) and
Line 55:		Line 55:
	[[File:Puzzle_graphical1.png]]		[[File:Puzzle_graphical1.png]]

	The graphical visualisation is achieved, with very little effort, by writing, in the DEFINITIONS section, the following animation function, as well as the image declaration list:		The graphical visualisation is achieved with very little effort by writing in the DEFINITIONS section, the following animation function, as well as the image declaration list:

	ANIMATION_FUNCTION == ( {r,c,i\|r:1..dim & c:1..dim & i=0} <+ board);		ANIMATION_FUNCTION == ( {r,c,i\|r:1..dim & c:1..dim & i=0} <+ board);
Line 68:		Line 68:
	ANIMATION_IMG8 == "images/sm_8.gif"; /* square with lightblue 8 inside */		ANIMATION_IMG8 == "images/sm_8.gif"; /* square with lightblue 8 inside */

	Each of the three integer types in the signature can be replaced by a deferred or enumerated set, in which case our tool translates elements of this set into numbers. In case of enumerated sets, the number is position of the element in the definition of the set in the SETS clause. Deferred set elements are numbered internally by ProB, and this number is used. (Note, however, that the whole animation function has to be of the same type; otherwise the animator will complain about a type error.) To avoid having to produce images for simple strings, one can use a declaration		Each of the three integer types in the signature can be replaced by a deferred or enumerated set, in which case our tool translates elements of this set into numbers. In the case of enumerated sets, the number is the position of the element in the definition of the set in the SETS clause. Deferred set elements are numbered internally by ProB, and this number is used. (Note however, that the whole animation function has to be of the same type; otherwise the animator will complain about a type error.) To avoid having to produce images for simple strings, one can use a declaration
	ANIMATION_STRx == "my string" to define image with number x to be automatically generated from the given string.		ANIMATION_STRx == "my string" to define image with number x to be automatically generated from the given string.

Line 78:		Line 78:
	where P is a predicate which gives img a value depending on row and col.		where P is a predicate which gives img a value depending on row and col.

	* Another useful pattern is to write one function for default images, and then use the override operator to replace the default images only when needed:		* Another useful pattern is to write one function for default images and then use the override operator to replace the default images only when needed:
	DefaultImages <+ CurrentImages		DefaultImages <+ CurrentImages
	This was used in the 8-Puzzle, by setting as default the empty square (image 0) overriden by the partially defined board function.		This was used in the 8-Puzzle by setting as default the empty square (image 0), which is then overriden by the partially defined board function.

	* '''or''' to write multiple definitions of the animation function. More clearly, we define one animation function for default images and another one for current images as follows:		* '''or''' to write multiple definitions of the animation function. More clearly, we define one animation function for default images and another one for current images as follows:
Line 88:		Line 88:

	This was used next in the Sudoku example.		This was used next in the Sudoku example.
	* Translation Predicates between user sets and numbers (extension above can directly handle user sets, but does not work well if we need a special image for undefined,...)		* Translation Predicates between user sets and numbers (extension above can directly handle user sets but does not work well if we need a special image for undefined,...)

	== Further Examples ==		== Further Examples ==
Line 133:		Line 133:


	The left side of the following Figure shows the non-graphical animation of the machine scheduler and the right side its graphical animation obtained using ProB.		The left side of the following Figure shows the non-graphical animation of the machine scheduler, and the right side shows its graphical animation obtained using ProB.

	[[File:scheduler_graphvis1.png]]		[[File:scheduler_graphvis1.png]]

	The graphical visualisation is done by writing, in the DEFINTIONS section, the following animation function. Here, we need to map PID elements to image numbers.		The graphical visualisation is done by writing in the DEFINTIONS section the following animation function. Here, we need to map PID elements to image numbers.

	IsPidNrci == p=process1 & i=1) or (p=process2 & i=2) or (p=process3 & i=3));		IsPidNrci == p=process1 & i=1) or (p=process2 & i=2) or (p=process3 & i=3));
Line 163:		Line 163:

	=== Sudoku ===		=== Sudoku ===
	Using ProB, we can also solve Sudoku puzzles. The machine has the variable Sudoku9 of type 1..fullsize-->(1..fullsize+->NRS), where NRS is an enumerate set {n1, n2, ...} of cardinality fullsize.		Using ProB we can also solve Sudoku puzzles. The machine has the variable Sudoku9 of type 1..fullsize-->(1..fullsize+->NRS), where NRS is an enumerate set {n1, n2, ...} of cardinality fullsize.

	The animation function is as follows:		The animation function is as follows:
Line 178:		Line 178:
	);		);

	The following Figure shows the non-graphical visualisation of a particular puzzle (left), ~~then~~ the graphical visualisation of the puzzle (middle), as well as the visualisation of the solution found by ProB after a couple of seconds (right).		The following Figure shows the non-graphical visualisation of a particular puzzle (left), the graphical visualisation of the puzzle (middle), as well as the visualisation of the solution found by ProB after a couple of seconds (right).

	[[File:Sudoku_graphvis1.png]]		[[File:Sudoku_graphvis1.png]]


	Note that it would have been nice to be able to replace Nri inside the animation function simply by i = Sudoku9(r)(c). While our visualisation algorithm can automatically convert set elements to numbers, the problem is that there is a type error in the override: the left-hand side is a function of type INTEGERINTEGER+->INTEGER while the right-hand side now becomes a function of type INTEGERINTEGER+->NRS. One solution is to write multiple definitions of the animation function. In addition to the standard animation function, we can define a default background animation function. The standard animation function will override the default animation function, but the overriding is done within the graphical animator and not within a B formula. In this way, one can now rewrite the above animation as follows:		Note that it would have been nice to be able to replace Nri inside the animation function simply by i = Sudoku9(r)(c). While our visualisation algorithm can automatically convert set elements to numbers, the problem is that there is a type error in the override: the left-hand side is a function of type INTEGERINTEGER+->INTEGER, while the right-hand side now becomes a function of type INTEGERINTEGER+->NRS. One solution is to write multiple definitions of the animation function. In addition to the standard animation function, we can define a default background animation function. The standard animation function will override the default animation function, but the overriding is done within the graphical animator and not within a B formula. In this way, one can now rewrite the above animation as follows:

	ANIMATION_FUNCTION_DEFAULT == ( {r,c,i\|r:1..fullsize & c:1..fullsize & i=0} );		ANIMATION_FUNCTION_DEFAULT == ( {r,c,i\|r:1..fullsize & c:1..fullsize & i=0} );