// **************************************************************************
//
//    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
//
// **************************************************************************
//
//  Connect Four (Vier Gewinnt)
//
// Here is a short summary of [Alli88], where many important observations
// on the Connect-Four game were made.
//
// The first result is that player White has no winning strategy on boards
// with 2n rows and m<=6 columns, since the following rules form a strategy
// for player Black to prevent White from winning (stated for 6 columns):
//
//   (1) If White inserts a man in one of the columns {1,2,5,6} at row r,
//       put a man in the same column at row r+1.
//   (2) If White inserts a man in one of the columns {3,4} at row 1,
//       put a man in the other column at row 1.
//   (3) If White inserts a man in one of the columns {3,4} at row r>1,
//       put a man in the same column at row r+1.
//
// Using these rules, Black will have the fields with even rows in columns {1,2,5,6}
// and one of the columns in {3,4}, and the fields with odd rows in the other column
// of {3,4}. Thus, player White can not have four connected men.
//
// The above strategy is essentially based on the follow-up rule, which means that
// the same column is selected. This way, vertical groups are directly prevented,
// and if also horizontal ones are disturbed in some way, there is only the chance
// to achieve diagonal groups. However, this is also not possible if the follow-up
// rule is played accordingly. Hence, the question concentrates on disturbing the
// construction of a horizontal group while following the follow-up rule...
//
// The follow-up rule tells us furthermore that one of the players can occupy all
// the even fields and the other one the odd fields if the number of empty fields
// is even. Thus, if a special square is wanted, one can play the follow-up
// strategy to finally receive that square...
//
// Black can also use a follow-up strategy to prevent White from winning on a
// 2n x 7 board if White does not start the game in the middle column.
//
//
// However, this does not mean that player Black has a strategy to win. Using
// brute-force state space traversals, we found that player Black has a winning
// strategy on the 4x6 board, but not on the 4x4 and 4x5 boards. On the 4x5 board,
// however, player Black has two winning states of the five possible states that
// appear after the first move (of player White) in the game (these are the
// corner fields). Hence, Black has still good chances to win on the 4x5 board
// as well.
//
// Moreover, [Alli88] shows that player White has a winning strategy on the
// 6x7 board if White follows the following rules:
//
//   (1) If there is a winning move, make it.
//   (2) If the opponent can win at a square by his next move, play that move first.
//   (3) Taking the central square is more important than other fields.
//   (4) Taking corner squares is more important than taking squares on the edges.
//
// It has been shown in [Alli88] that White has no winning strategy on a 4x7 board,
// but it has a winning strategy on a 6x7 board. Moreover, it is easily seen that
// White will only save its winning strategy by first inserting a man in the middle
// column 3. Otherwise, Black can play the follow-up strategy together with a strategy
// to disturb the construction of horizontal groups, and therefore is able to prevent
// White from winning.
// ------------------------------------------------------------

package ConnectFour;

import ConnectFour.*;

macro rows = 4;
macro cols = 6;

module ConnectFour(
      nat{cols} col_black, ?col_white,
      [cols][rows]bool black, [cols()][rows()]bool white,
      event blackHasWon, event whiteHasWon, bool turnWhite,
      nat{cols} c, nat{rows} r, nat{rows()} !mr) {
    do {
        c = (turnWhite?col_white:col_black);
        // check whether selected row is already full
        if( !(black[c][rows-1] | white[c][rows-1]) ) {
            // find the least free row r in column c
            if(not(black[c][0] or white[c][0]))
                r = 0;
            else
                for( i=1 .. rows-1 )
                    if(black[c][i-1] or white[c][i-1])
                        if(not(black[c][i] or white[c][i]))
                            r = i;
            // insert coin in field [c][r] and check winning cond.
            if(turnWhite) {
                next(white[c][r]) = true;
                HasWon(white,c,r,whiteHasWon);
            } else {
                next(black[c][r]) = true;
                HasWon(black,c,r,blackHasWon);
            }
            // toggle turn variable
            next(turnWhite) = !turnWhite;
        }
        pause;
    } while(!(blackHasWon | whiteHasWon));
}