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