Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Conway.vdmsl Sprache: VDM

Original von: 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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.