// ************************************************************************** // // 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 // // ************************************************************************** // // Single Row NIM Game with Strategic Player A // // N matches is put on a desk. Two players A and B then take either 1,2, // or 3 matches in alternating turns from this pile. The player who will // take the last match has won. // // Hint: the strategy is to choose a number of matches such that the // remaining matches is a multiple of four. This is always possible for // player A if initially the number of matches is not a multiple of four. // Otherwise, player B will have the winning strategy. The implementation // below will then simply allow player A to do a move where no matches are // taken. This will never happen afterwards. // // ************************************************************************** macro N = 21; module SingleRowNIM( nat{4} numA, numB, nat{N+1} matches, bool turnA ) { turnA = true; matches = N; while(matches>0) { if(turnA) { numA = (matches % 4); next(matches) = matches-numA; next(turnA) = not turnA; } else { if(0<numB & numB<=matches) { next(matches) = matches-numB; next(turnA) = not turnA; } } pause; } } satisfies { A_always_wins: assert A G (matches==0 -> !turnA); }