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