• Special Pages
• User

Help

# Game of Life

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.

```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
```

We believe this to be quite compact. In the future we hope to be able to remove the need to add the predicate #(a2,b2).((a2,b2):alive & neighbour(u2,v2,a2,b2)) by improving ProB's constraint solver for cardinality constraints on set comprehensions. You may want to compare this to an 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. This leads to the following B model (where we have also added an alternate definition of the neighbourhood relationship):

```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
```

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