spec module ExposedList = Arrayset with Node <- Cell;
spec module UnexposedList = List with Node <- Cell;

spec module Board
{
    format Cell;
    specvar MarkedCells, MinedCells, 
            ExposedCells, UnexposedCells, U : Cell set;
    specvar init, gameOver, peeking : bool;
    default I : pre(not proc *.init() && not proc UnexposedList.*() &&
                    not proc View.makeWcf() && not proc View.makeBox()) = init;
    default NP : pre(not proc View.draw*() ||
                     proc View.drawFieldInitial() ||
                     proc View.drawFieldEnd() &&
                     not proc UnexposedList.*()) = not peeking;

    // constructor
    proc init(size:int; mineCount:int) 
      requires card(ExposedCells)=0 & card(UnexposedCells) = 0 &
               card(ExposedList.Content)=0 & card(UnexposedList.Content)=0 &
               card(U)=0 & disjoint(MarkedCells, ExposedCells) & not gameOver
      modifies U, UnexposedCells, UnexposedList.Content, MinedCells, init,
               ExposedList.Content, ExposedList.setInit, UnexposedList.Iter,
               peeking
      calls UnexposedList, ExposedList
      ensures init' & (UnexposedCells' <= U') & 
              card(ExposedCells') = 0 & 
              disjoint(MarkedCells', ExposedCells') & not peeking';

    proc assignInitialMines(size:int; mineCount:int)
      requires not gameOver & disjoint(MarkedCells, ExposedCells) &
               card(ExposedCells)=0 & (ExposedCells = ExposedList.Content) & 
               (UnexposedCells = UnexposedList.Content) & 
               disjoint(MarkedCells, ExposedCells) & 
               ExposedList.setInit & not peeking & card(UnexposedList.Iter) = 0
      modifies MinedCells
      ensures true;

    // read state; note that ensuring @repinv() is extraneous, because
    // we have empty modifies clauses, and don't depend on the invariant.
    // it might be useful for getExposed, though.
    proc getMined(c:Cell) returns m:bool suspends NP
      requires (c in U) & (card(c)=1)
      ensures (c in MinedCells) <=> m';
    proc getExposed(c:Cell) returns m:bool suspends NP
      requires (c in U) & (card(c)=1)
      ensures (c in ExposedCells) <=> m';
    proc getMarked(c:Cell) returns m:bool suspends NP
      requires (c in U) & (card(c)=1)
      ensures (c in MarkedCells) <=> m';

    // ensure true

    proc countAdj(i:int; j:int) returns n : int suspends NP ensures true;
    proc getN() returns n : int suspends I, NP ensures true;
    proc getCell(i:int; j:int) returns c:Cell 
                               ensures (card(c') = 1) & (c' in U);
    proc getI(c:Cell) returns i:int suspends NP ensures true;
    proc getJ(c:Cell) returns j:int suspends NP ensures true;

    // mutate state
    proc setMined(c:Cell; v:bool) 
      requires (c in U) & (card(c)=1) & /* !gameOver & */ 
               disjoint(MinedCells, ExposedCells) &
               not (c in ExposedCells)
      modifies MinedCells 
      ensures (v <=> (c in MinedCells')) &
              (MinedCells' <= MinedCells + c) &
              disjoint(MinedCells', ExposedCells);

    proc setExposed(c:Cell; v:bool)
      requires (c in U) & (card(c)=1)
      modifies ExposedCells, UnexposedCells, 
               ExposedList.Content, UnexposedList.Content,
               UnexposedList.Iter, Board.gameOver
      calls ExposedList, UnexposedList
      ensures (v => ((ExposedCells' = ExposedCells + c) &
                     (UnexposedCells' = UnexposedCells - c) &
                     (UnexposedList.Iter' = UnexposedList.Iter - c))) & 
              ((not v) => ((ExposedCells' = ExposedCells - c) &
                           (UnexposedCells' = UnexposedCells + c))) & 
     /* need this because don't get derived set defns outside this module: */
              (UnexposedCells' <= U');

    proc setMarked(c:Cell; v:bool) 
      requires (c in U) & (card(c)=1) 
      modifies MarkedCells 
      ensures (v <=> (c in MarkedCells')) & 
              (MarkedCells' <= MarkedCells + c);

    proc setGameOver()
      modifies gameOver
      ensures gameOver';

    proc isGameOver() returns rv:bool
      ensures rv' <=> gameOver;

    // no support for arrays in specs...
    proc hasTrueNeighbourIn(i:int; j:int; N:int; b:bool[]) returns v:bool ensures true;
    proc visit(i:int; j:int) ensures true;
    proc cellsToSee(i0:int; j0:int) returns m:bool[] ensures true;

    proc revealAllUnexposed()
      requires gameOver 
      modifies ExposedCells, UnexposedCells
      ensures card(UnexposedCells') = 0;

    proc peek() 
      requires init & ExposedList.setInit 
      modifies UnexposedList.Iter, peeking
      calls UnexposedList, View
      ensures not peeking';
}