Overture Tool

Formal Modelling in VDM

Overture Tool

Go to our GitHub Profile

Follow @overturetool

ConwayGameLifeSL

Author: Nick Battle, Peter Gorm Larsen and Claus Ballegaard Nielsen (animation)

Conway’s Game of Life The universe of the Game of Life is an infinite two-dimensional orthogonal grid of square cells, each of which is in one of two possible states, alive or dead. Every cell interacts with its eight neighbours, which are the cells that are horizontally, vertically, or diagonally adjacent. At each step in time, the following transitions occur:

The initial pattern constitutes the seed of the system. The first generation is created by applying the above rules simultaneously to every cell in the seed-births and deaths occur simultaneously, and the discrete moment at which this happens is sometimes called a tick (in other words, each generation is a pure function of the preceding one). The rules continue to be applied repeatedly to create further generations.

Properties Values
Language Version: vdm10
Entry point : Conway`periodN(PULSAR,3)
Entry point : Conway`tests()
Entry point : Conway`generations(130,DIEHARD)
Entry point : gui_Graphics`generations_animate(130,DIEHARD)

Conway.vdmsl

/**
 * Conways Game of Life
 *
 * The universe of the Game of Life is an infinite two-dimensional orthogonal grid of square cells,
 * each of which is in one of two possible states, alive or dead. Every cell interacts with its 
 * eight neighbours, which are the cells that are horizontally, vertically, or diagonally adjacent.
 * At each step in time, the following transitions occur:
 *
 *   Any live cell with fewer than two live neighbours dies, as if caused by under-population.
 *   Any live cell with two or three live neighbours lives on to the next generation.
 *   Any live cell with more than three live neighbours dies, as if by overcrowding.
 *   Any dead cell with exactly three live neighbours becomes a live cell, as if by reproduction.
 *
 * The initial pattern constitutes the seed of the system. The first generation is created by 
 * applying the above rules simultaneously to every cell in the seed-births and deaths occur 
 * simultaneously, and the discrete moment at which this happens is sometimes called a tick 
 * (in other words, each generation is a pure function of the preceding one). The rules continue 
 * to be applied repeatedly to create further generations.
 *
 * Modelled in VDM-SL by Nick Battle and Peter Gorm Larsen and animation made by 
 * Claus Ballegaard Nielsen
 */

module Conway 
exports all

definitions

values
	GENERATE	= 3;		-- Number of neighbours to cause generation
	SURVIVE		= {2, 3};	-- Numbers of neighbours to ensure survival, else death
	
types
	Point ::				-- Plain is indexed by integers
		x : int
		y : int;
		
	Population = set of Point;
	
	
functions
	-- Generate the Points around a given Point
	around: Point -> set of Point
	around(p) ==
		{ mk_Point(p.x + x, p.y + y) | x, y in set { -1, 0, +1 }
			& x <> 0 or y <> 0 }
	post card RESULT < 9;
	
	-- Count the number of live cells around a given point 
	neighbourCount: Population * Point -> nat
	neighbourCount(pop, p) ==
		card { q | q in set around(p) & q in set pop }
	post RESULT < 9;

	-- Generate the set of empty cells that will become live
	newCells: Population -> set of Point
	newCells(pop) ==
		dunion
		{
			{ q | q in set around(p)
				  & q not in set pop and neighbourCount(pop, q) = GENERATE }		
			| p in set pop
		}
	post RESULT inter pop = {};		-- None currently live
		
	-- Generate the set of cells to die
	deadCells: Population -> set of Point
	deadCells(pop) ==
		{ p | p in set pop
			& neighbourCount(pop, p) not in set SURVIVE }
	post RESULT inter pop = RESULT;	-- All currently live
	
	-- Perform one generation
	generation: Population -> Population
	generation(pop) ==
		(pop \ deadCells(pop)) union newCells(pop);

	-- Generate a sequence of N generations 
	generations: nat1 * Population -> seq of Population
	generations(n,pop) ==
		let new_p = generation(pop)
		in
			if n = 1
			then [new_p] 
			else [new_p] ^ generations(n-1,new_p)
	measure measureGenerations;
     
	measureGenerations: nat1 * Population -> nat
	measureGenerations(n,-) == n;
	
    -- Generate an offset of a Population (for testing gliders)
	offset: Population * int * int -> Population
	offset(pop, dx, dy) ==
		{ mk_Point(x + dx, y + dy) | mk_Point(x, y) in set pop };
		
	-- Test whether two Populations are within an offset of each other
	isOffset: Population * Population * nat1 -> bool
	isOffset(pop1, pop2, max) ==
		exists dx, dy in set {-max, ..., max}
			& (dx <> 0 or dy <> 0) and offset(pop1, dx, dy) = pop2;
			
	-- Test whether a game is N-periodic
	periodN: Population * nat1 -> bool
	periodN(pop, n) == (generation ** n)(pop) = pop;

	-- Test whether a game disappears after N generations
	disappearN: Population * nat1 -> bool
	disappearN(pop, n) ==
		(generation ** n)(pop) = {};
 
	-- Test whether a game is N-gliding within max cells
	gliderN: Population * nat1 * nat1 -> bool
	gliderN(pop, n, max) ==
		isOffset(pop, (generation ** n)(pop), max);
		
 	-- Versions of the three tests that check that N is the least value
	periodNP: Population * nat1 -> bool
	periodNP(pop, n) ==
		{ a | a in set {1, ..., n} & periodN(pop, a) } = {n};

	disappearNP: Population * nat1 -> bool
	disappearNP(pop, n) ==
		{ a | a in set {1, ..., n} & disappearN(pop, a) } = {n};
		
	gliderNP: Population * nat1 * nat1 -> bool
	gliderNP(pop, n, max) ==
		{ a | a in set {1, ..., n} & gliderN(pop, a, max) } = {n};
 
	
-- Test games from http://en.wikipedia.org/wiki/Conway%27s_Game_of_Life
values
	BLOCK = { mk_Point(0,0), mk_Point(-1,0), mk_Point(0,-1), mk_Point(-1,-1)};

	BLINKER = { mk_Point(-1,0), mk_Point(0,0), mk_Point(1,0) };
	
	TOAD = BLINKER union { mk_Point(0,-1), mk_Point(-1,-1), mk_Point(-2,-1) };
	
	BEACON = { mk_Point(-2,0), mk_Point(-2,1), mk_Point(-1,1), mk_Point(0,-2),  
	           mk_Point(1,-2), mk_Point(1,-1 )};
            
	PULSAR = let quadrant = { mk_Point(2,1), mk_Point(3,1), mk_Point(3,2),
                           mk_Point(1,2), mk_Point(1,3), mk_Point(2,3),
                           mk_Point(5,2), mk_Point(5,3), mk_Point(6,3), mk_Point(7,3),
                           mk_Point(2,5), mk_Point(3,5), mk_Point(3,6), mk_Point(3,7) }
			in
				quadrant union
				{ mk_Point(-x, y)| mk_Point(x, y) in set quadrant } union
				{ mk_Point(x, -y)| mk_Point(x, y) in set quadrant } union
				{ mk_Point(-x, -y)| mk_Point(x, y) in set quadrant };
				
  DIEHARD = {mk_Point(0,1),mk_Point(1,1),mk_Point(1,0),
             mk_Point(0,5),mk_Point(0,6),mk_Point(0,7),mk_Point(2,6)};
      
  GLIDER = { mk_Point(1,0), mk_Point(2,0), mk_Point(3,0), mk_Point(3,1), mk_Point(2,2) };      
       
  GOSPER_GLIDER_GUN = { mk_Point(2,0), mk_Point(2,1), mk_Point(2,2), mk_Point(3,0), mk_Point(3,1),
        mk_Point(3,2), mk_Point(4,-1), mk_Point(4,3), mk_Point(6,-2), mk_Point(6,-1),
        mk_Point(6,3), mk_Point(6,4), mk_Point(16,1), mk_Point(16,2), mk_Point(17,1),
        mk_Point(17,2), mk_Point(-1,-1), mk_Point(-2,-2), mk_Point(-2,-1), mk_Point(-2,0),
        mk_Point(-3,-3), mk_Point(-3,1), mk_Point(-4,-1), mk_Point(-5,-4), mk_Point(-5,2),
        mk_Point(-6,-4), mk_Point(-6,2), mk_Point(-7,-3), mk_Point(-7,1), mk_Point(-8,-2),
        mk_Point(-8,-1), mk_Point(-8,0), mk_Point(-17,-1), mk_Point(-17,0), mk_Point(-18,-1),
        mk_Point(-18,0)};
        
functions
	tests: () -> seq of bool
	tests() ==
	[
		periodNP(BLOCK,	1),	-- ie. constant
		periodNP(BLINKER,2),
		periodNP(TOAD,	2),
		periodNP(BEACON, 2),
		periodNP(PULSAR, 3),
		gliderNP(GLIDER, 4, 1),
		disappearNP(DIEHARD, 130)
	];
	          
             
end Conway
    

Graphics.vdmsl

module gui_Graphics 

imports from Conway all

exports all
definitions

types
	Configuration ::
		gridSide : int
		sleepTime : int
		pop : Conway`Population;

functions
	generations_animate: nat1 * Configuration -> seq of Conway`Population
	generations_animate(n,conf) == 
		let - = initialise(conf.gridSide, conf.sleepTime) 
		 in
		  let patterns =  Conway`generations(n, conf.pop) 
		   in 
		    animate_step(patterns);

	animate_step : seq of Conway`Population -> seq of Conway`Population
	animate_step(pop) ==
		if pop = [] 
		then []
		else
			let - = {newLivingCell(cell.x, cell.y)| cell in set hd pop} 
			 in		
			  let - = newRound() 
			   in
	 		    animate_step(tl pop) 
	measure measure_animate_step;
	
	measure_animate_step: seq of Conway`Population -> nat
	measure_animate_step(list) == len list;

	initialise: nat1 * nat1 -> int
  initialise(gridSideCount, sleepTime)== is not yet specified;
    
  newLivingCell:  int * int -> int
  newLivingCell(x,y)== is not yet specified;
    
  newRound: () -> int
  newRound()== is not yet specified;

values
	BLOCK = mk_Configuration(4, 500, Conway`BLOCK);

	BLINKER = mk_Configuration(5, 500, Conway`BLINKER);
	
	TOAD = mk_Configuration(6, 500, Conway`TOAD );
	
	BEACON = mk_Configuration(8, 500, Conway`BEACON);
            
	PULSAR =  mk_Configuration(17, 1000, Conway`PULSAR);
				
  DIEHARD = mk_Configuration(33, 300, Conway`DIEHARD);
      
  GLIDER = mk_Configuration(40, 100, Conway`GLIDER);      
       
  GOSPER_GLIDER_GUN = mk_Configuration(40, 50, Conway`GOSPER_GLIDER_GUN);

end gui_Graphics