module cw/life
open std/ord

-- based on a model by Bill Thies <thies@mit.edu>, Manu Sridharan <msridhar@mit.edu>


sig Cell {
  right, below : option Cell,  -- option specifies a 0/1 multiplicity
  above, left : option Cell,
  neighbours: set Cell
}
fact { all c: Cell |
  c.above = c.~below  && 
  c.left = c.~right &&
  c.neighbours=
       c.above.left   + c.above +  c.above.right +
       c.left         +            c.right +
       c.below.left   + c.below +  c.below.right
}
static sig Root extends Cell {} 

fact Connected { Root.*(right + below) = Cell } -- *r = r + ^r
fact Acyclic { all c: Cell | c !in c.^(right + below) }
fact Square { #Root.*right = #Root.*below }  
-- #r denotes the cardinality of the relation r
fact Symetric { all c: Cell | c.below.right = c.right.below }
fact Filled { all c: Cell | some c.below && some c.right => some c.below.right }
fun isTiled () { some Cell }

run isTiled for 9 

sig Gen { live : set Cell }

fun LiveNeighbours(g: Gen, c: Cell) : set Cell {
    result =  c.neighbours  & g.live }

fun Trans(now, next: Gen, c: Cell) {
   let livers = LiveNeighbours(now, c) |
    // dead cells with 3 live neighbours becomes live
    (c !in now.live && #livers = 3) =>
       c in next.live
  else (
    // live cells with 2 or 3 live neighbours stays alive
    (c in now.live && (#livers = 2 || #livers = 3)) =>
      c in next.live else c !in next.live
    )
}

fact Life {
  all g : Gen - Ord[Gen].last |
    let next = OrdNext(g) |
      all c: Cell |
        Trans(g,next,c)
}

fun StillAlive () {
 some Ord[Gen].last.live 
}

run StillAlive for 9 but 5 Gen