spec module Controller
{
    specvar flagSwitchOn : bool;
    default G = Board.gameOver | disjoint (Board.MinedCells, Board.ExposedCells);

    proc revealCell(d:ControllerConfig; c:Cell) 
      requires (c in Board.U) & (card(c) = 1) & not (c in Board.MinedCells) & disjoint (Board.MinedCells, Board.ExposedCells) & 
               Board.init
      modifies Board.ExposedCells, Board.UnexposedCells, Board.gameOver
      calls Board, View
      ensures disjoint(Board.MinedCells', Board.ExposedCells') & (Board.UnexposedCells' <= Board.U');
    proc reveal(d:ControllerConfig; i0:int; j0:int) returns done:bool 
      requires (Board.UnexposedCells <= Board.U) & 
               disjoint(Board.MinedCells, Board.ExposedCells) & not Board.gameOver 
      modifies Board.ExposedCells, Board.UnexposedCells, Board.gameOver
      calls Board, View
      ensures (Board.UnexposedCells' <= Board.U') &
              (done' <=> Board.gameOver') &
              (Board.gameOver' | disjoint(Board.MinedCells', Board.ExposedCells'));
    proc click(d:ControllerConfig; i:int; j:int) 
      returns done:bool 
      requires (Board.UnexposedCells <= Board.U) &
               Board.init & not Board.gameOver
      modifies Board.ExposedCells, 
               Board.UnexposedCells,
               Board.MarkedCells, Board.gameOver
      calls Board, View
      ensures (done' <=> Board.gameOver') & 
              (Board.gameOver' | disjoint(Board.MinedCells', Board.ExposedCells')) & 
              (Board.UnexposedCells' <= Board.U');
    proc handleKey(c:char) returns done:bool 
      requires not Board.gameOver & disjoint(Board.MinedCells, Board.ExposedCells) & (Board.UnexposedCells <= Board.U)
      modifies Board.gameOver, Board.peeking calls Board 
      ensures (done' <=> Board.gameOver') & not Board.peeking' &
              (Board.UnexposedCells' <= Board.U') &
              (Board.gameOver' | disjoint(Board.MinedCells', Board.ExposedCells'));
    proc handleMouse(d:ControllerConfig; x1:int; y1:int; 
                     x2:int; y2:int) returns done:bool 
      requires not Board.gameOver &
               (Board.UnexposedCells <= Board.U)
      modifies flagSwitchOn, Board.ExposedCells, 
               Board.UnexposedCells, 
               Board.MarkedCells, Board.gameOver
      calls View
      ensures (done' <=> Board.gameOver') & 
              (Board.gameOver' | disjoint(Board.MinedCells', Board.ExposedCells')) &
              (Board.UnexposedCells' <= Board.U');
    proc loop() 
      requires Board.init & not Board.gameOver &
               (Board.UnexposedCells <= Board.U)
      modifies Board.ExposedCells, 
               Board.UnexposedCells,
               Board.MarkedCells, flagSwitchOn, Board.gameOver, Board.peeking
      calls Controller
      ensures true;
    proc flagCell(d:ControllerConfig; c:Cell) 
      requires (c in Board.U) & (card(c) = 1)
      modifies Board.MarkedCells
      calls Board, View
      ensures true;
    proc locateClicks(x1:int;y1:int; x2:int;y2:int) returns r:int 
      calls View
      ensures true;
    proc lastClickX() returns x:int ensures true;
    proc lastClickY() returns y:int ensures true;
    proc init(i:int; j:int; mines:int) 
      requires Board.init
      calls View
      ensures true;

    proc end() requires Board.gameOver ensures true;
}