Quelle  Conway.vdmsl   Sprache: VDM

/**
 * 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