```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
//  NIM Game
//
//  A couple of matches is distributed in rows on a board "Board" such that
//  row "i" contains 2*i+1 matches. In alternation, two players A and B then
//  then take an arbitrary number of matches from one row. The player who
//  will take the last match has won the game.
//
//  In module MultiRowNIM below, the variable turnA holds iff its player A's
//  turn, and in this case the inputs numA and rowA encode player A's
//  move: player A will take numA matches from rowA. In case that this
//  should not be possible, player A is asked once more for a legal move,
//  otherwise, the next turn is player B's move, which is handled in the
//  same way by the inputs numB and rowB, respectively.
//
// **************************************************************************

macro rows = 5;
macro size = rows() + rows();
macro XOR(x,y)= bv2nat(nat2bv(x,size-1) ^ nat2bv(y,size()-1));

module MultiRowNIM(
nat{rows} rowA, ?rowB,
nat{size} numA, ?numB,
[rows]nat{size} Board,
bool turnA, foundRow
) {
// Initialization
turnA = true;
for(i=0..rows-1) Board[i] = 2*i+1;

// now play the game
while( !forall(i=0..rows-1) (Board[i]==0) /* end of game */ ) {
if(turnA) {
// compute XOR of all rows
numA = 0;
for(i=0..rows-1) {
next(numA) = XOR(Board[i],numA);
pause;
}
// find row to take matches from
rowA = 0;
foundRow = false;
for (i=0..rows-1) {
if(Board[i]>=XOR(Board[i],numA) & not(foundRow)) {
next(rowA) = i;
next(numA) = Board[i]-XOR(Board[i],numA);
next(foundRow) = true;
}
pause;
}
// make the move
next(Board[rowA]) = Board[rowA]-numA;
next(turnA) = not turnA;
} else {
// B's moves are only accepted if reasonable
// caution: this may yield an infinite game!
if(numB<=Board[rowB]) {
next(Board[rowB]) = Board[rowB]-numB;
next(turnA) = not turnA;
}
}
pause;
}
} satisfies {
A_will_always_win: assert
A G (
(forall(i=0..rows-1) (Board[i]==0)) /* end of game */
-> !turnA);
}
```