Game of Life - Revision history

Jens Bendisposto at 06:52, 9 September 2013

2013-09-09T06:52:12Z

← Older revision		Revision as of 06:52, 9 September 2013
Line 25:		Line 25:
	</pre>		</pre>

	We believe this to be quite compact. In the future we hope to be able to remove the need to add the predicate <tt>#(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) <tt> by improving ProB's constraint solver for cardinality constraints on set comprehensions.		We believe this to be quite compact. In the future we hope to be able to remove the need to add the predicate <tt>#(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) </tt> by improving ProB's constraint solver for cardinality constraints on set comprehensions.
	You may want to compare this to an [http://sourceforge.net/p/asmeta/code/2606/tree/asm_examples/examples/conwayGameOfLife/ ASM specification found here] and described on pages 39-40 in Egon Börger and Robert Stärk, Abstract State Machines, A Method for High-Level System Design and Analysis, Springer-Verlag 2003, (ISBN 3-540-00702-4).		You may want to compare this to an [http://sourceforge.net/p/asmeta/code/2606/tree/asm_examples/examples/conwayGameOfLife/ ASM specification found here] and described on pages 39-40 in Egon Börger and Robert Stärk, Abstract State Machines, A Method for High-Level System Design and Analysis, Springer-Verlag 2003, (ISBN 3-540-00702-4).

Michael Leuschel at 07:40, 5 September 2013

2013-09-05T07:40:33Z

← Older revision		Revision as of 07:40, 5 September 2013
Line 26:		Line 26:

	We believe this to be quite compact. In the future we hope to be able to remove the need to add the predicate <tt>#(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) <tt> by improving ProB's constraint solver for cardinality constraints on set comprehensions.		We believe this to be quite compact. In the future we hope to be able to remove the need to add the predicate <tt>#(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) <tt> by improving ProB's constraint solver for cardinality constraints on set comprehensions.
	You may want to compare this to an [http://sourceforge.net/p/asmeta/code/2606/tree/asm_examples/examples/conwayGameOfLife/ ASM specification found here] and described on ~~page 29~~ in Egon Börger and Robert Stärk, Abstract State Machines, A Method for High-Level System Design and Analysis, Springer-Verlag 2003, (ISBN 3-540-00702-4).		You may want to compare this to an [http://sourceforge.net/p/asmeta/code/2606/tree/asm_examples/examples/conwayGameOfLife/ ASM specification found here] and described on pages 39-40 in Egon Börger and Robert Stärk, Abstract State Machines, A Method for High-Level System Design and Analysis, Springer-Verlag 2003, (ISBN 3-540-00702-4).

	If you want to visualize the simulation using ProB's Tk graphical viewer one needs to add a definition for the animation function.		If you want to visualize the simulation using ProB's Tk graphical viewer one needs to add a definition for the animation function.

Michael Leuschel at 07:24, 5 September 2013

2013-09-05T07:24:17Z

← Older revision		Revision as of 07:24, 5 September 2013
Line 24:		Line 24:
	END		END
	</pre>		</pre>

			We believe this to be quite compact. In the future we hope to be able to remove the need to add the predicate <tt>#(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) <tt> by improving ProB's constraint solver for cardinality constraints on set comprehensions.
			You may want to compare this to an [http://sourceforge.net/p/asmeta/code/2606/tree/asm_examples/examples/conwayGameOfLife/ ASM specification found here] and described on page 29 in Egon Börger and Robert Stärk, Abstract State Machines, A Method for High-Level System Design and Analysis, Springer-Verlag 2003, (ISBN 3-540-00702-4).

	If you want to visualize the simulation using ProB's Tk graphical viewer one needs to add a definition for the animation function.		If you want to visualize the simulation using ProB's Tk graphical viewer one needs to add a definition for the animation function.

Michael Leuschel at 07:20, 5 September 2013

2013-09-05T07:20:25Z

← Older revision		Revision as of 07:20, 5 September 2013
Line 62:		Line 62:
	END		END
	</pre>		</pre>

			The following is a screenshot of ProB Tcl/Tk animating the above model:



			[[File:ProB_GameOfLife_Screenshot.png\|600px\|center]]

Michael Leuschel: Created page with 'This is a simple model of Conway's Game of Life. It was written for animation with ProB. One interesting aspect is that the simulation is unbounded, i.e., not restricted to some …'

2013-09-05T07:18:49Z

Created page with 'This is a simple model of Conway's Game of Life. It was written for animation with ProB. One interesting aspect is that the simulation is unbounded, i.e., not restricted to some …'

New page

This is a simple model of Conway's Game of Life.
It was written for animation with ProB. One interesting aspect is that the simulation is unbounded, i.e., not restricted to some pre-determined area of the grid.

<pre>
MACHINE gol
/* A simple B model of the Game of Life */
/* by Jens Bendisposto and Michael Leuschel */
ABSTRACT_CONSTANTS nc
PROPERTIES
/* neighbour count function: */
nc = %(a,b,alive).(a:INTEGER&b:INTEGER & alive <: INTEGER*INTEGER
| card({(xn,yn)| (xn,yn) : alive & neighbour(xn,yn,a,b)}))
VARIABLES alive
DEFINITIONS
neighbour(x,y,a,b) == (max({x-a,a-x}) : {0,1} & max({y-b,b-y}) : {0,1} & (x,y)/=(a,b));
INVARIANT
alive <: INTEGER * INTEGER & alive /= {}
INITIALISATION
alive := {(2,1),(2,2),(2,3)} /* blinker */
OPERATIONS
step = alive := {(u1,v1) | (u1,v1):alive & nc(u1,v1,alive) : {2,3} } \/
{(u2,v2) | #(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) & /* restrict enumeration to neighbours of alive */
(u2,v2)/:alive & nc(u2,v2,alive)=3 }
END
</pre>

If you want to visualize the simulation using ProB's Tk graphical viewer one needs to add a definition for the animation function.
This leads to the following B model (where we have also added an alternate definition of the neighbourhood relationship):

<pre>
MACHINE gol
/* A simple B model of the Game of Life */
/* by Jens Bendisposto and Michael Leuschel */
ABSTRACT_CONSTANTS nc
PROPERTIES
/* neighbour count function: */
nc = %(a,b,alive).(a:INTEGER&b:INTEGER & alive <: INTEGER*INTEGER
| card({(xn,yn)| (xn,yn) : alive & neighbour(xn,yn,a,b)}))
VARIABLES alive
DEFINITIONS
/* two alternate definitions of neighbour relationship; both work */
neighbour1(x,y,a,b) == (max({x-a,a-x}) : {0,1} & max({y-b,b-y}) : {0,1} & (x,y)/=(a,b));
neighbour(x,y,a,b) == ((x-a)**2 <= 1 & (y-b)**2 <=1 & (x,y)/=(a,b));
/* some simple patterns : */
blinker == {(2,1),(2,2),(2,3)} ; glider == {(1,2),(2,3),(3,1),(3,2),(3,3)} ;
SET_PREF_CLPFD == TRUE;
/* describing the animation function for the graphical visualization : */
wmin == min(dom(alive)\/{1}); wmax == max(dom(alive)\/{1});
hmin == min(ran(alive)\/{1}); hmax == max(ran(alive)\/{1});
ANIMATION_FUNCTION_DEFAULT == ( (wmin..wmax)*(hmin..hmax)*{0} );
ANIMATION_FUNCTION == ( alive * {1} );
ANIMATION_IMG0 == "images/sm_empty_box.gif";
ANIMATION_IMG1 == "images/sm_gray_box.gif"
INVARIANT
alive <: INTEGER * INTEGER & alive /= {}
INITIALISATION
alive := glider
OPERATIONS
step = alive := {(u1,v1) | (u1,v1):alive & nc(u1,v1,alive) : {2,3} } \/
{(u2,v2) | #(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) & /* restrict enumeration to neighbours of alive */
(u2,v2)/:alive & nc(u2,v2,alive)=3 }
END
</pre>