// **************************************************************************
//
//    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);
}