scope Model
{
    modules Board, ExposedList, UnexposedList, List, Arrayset;
    exports Board;
    invariant (Board.ExposedCells = ExposedList.Content) &
              (Board.UnexposedCells = UnexposedList.Content) & 
              (Board.init => ExposedList.setInit) &
              (Board.peeking | (card(UnexposedList.Iter) = 0));
}