Formal Modelling for Systems of Systems

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

This example illustrate Conways game of life (see http://en.wikipedia.org/wiki/Conway’s_Game_of_Life) which has has interesting emergent properties. A VDM-SL version of this example was produced by Nick Battle and Peter Gorm Larsen and Claus Ballegaard Nielsen produced a graphical user interface showing the evolution of life following the rules of the 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: 1.Any live cell with fewer than two live neighbours dies, as if caused by under-population. 2.Any live cell with two or three live neighbours lives on to the next generation. 3.Any live cell with more than three live neighbours dies, as if by overcrowding. 4.Any dead cell with exactly three live neighbours becomes a live cell, as if by reproduction. A CML version of this was produced by Peter Gorm Larsen but no graphical user interface is available at this stage. In addition, this CML model does not yet have any any reactive bahaviour so it cannot be animated in the Symphony tool at this stage.

```
/**
* 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.
*
* Originally modelled in VDM-SL by Nick Battle and Peter Gorm Larsen and animation made by
* Claus Ballegaard Nielsen. Current version in CML made by Peter Gorm Larsen.
*/
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)
]
```