| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/VDM/VDMSL/ConwayGameLifeSL/ (Wiener Entwicklungsmethode ©) Datei vom 13.4.2020 mit Größe 6 kB |
|
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 cell * 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 adja * 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_Po 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.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28