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