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

package ConnectFour;

macro rows = 4;
macro cols = 6;

module HasWon(
    [cols][rows()]bool player,
    nat{cols} c,
    nat{rows} r,
    event !has_won
) {
    // check vertical column of four
    if(r>=3) {
        if( player[c][r-1] & player[c][r-2] & player[c][r-3] )
            emit next(has_won);
    }
    // check south-west diagonal of four
    if(r>=3 and c>=3) {
        if(player[c-1][r-1] & player[c-2][r-2] & player[c-3][r-3] )
            emit next(has_won);
    }
    // check north-west diagonal of four
    if(r>=3 and c+3<=cols) {
        if(player[c+1][r-1] & player[c+2][r-2] & player[c+3][r-3] )
         emit next(has_won);
    }
    // check north-east diagonal of four
    if(r+3<=rows and c+3<=cols()) {
        if(player[c+1][r+1] & player[c+2][r+2] & player[c+3][r+3])
            emit next(has_won);
    }
    // check south-east diagonal of four
    if(r+3<=rows and c>=3) {
            if(player[c-1][r+1] & player[c-2][r+2] & player[c-3][r+3])
                emit next(has_won);
    }
}