spec module Main
{
    // TODO: mark the program entry point, so that sets can be assumed {}.
    proc main()
      suspends Board.I, Board.NP
      requires card(Board.ExposedCells)=0 & card(Board.UnexposedCells) = 0 &
               card(Board.U)=0 & not Board.peeking & not Board.gameOver &
               disjoint(Board.MarkedCells, Board.ExposedCells) 
      modifies Board.U, Board.ExposedCells, Board.MarkedCells, 
               Board.UnexposedCells, Board.peeking, 
               Board.MinedCells, Board.init, Board.gameOver, 
               Controller.flagSwitchOn
      calls Board, Controller 
      ensures true;
}