// **************************************************************************
//
//    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
//
// **************************************************************************
//
//  Solitaire game on a NxN square
//
//  parameters
//      - N: size of the field
//      - X0: x-coordinate of initial free field
//      - Y0: y-coordinate of initial free field
//
//  ----------------------------------------------------------------
//  here are some results:
//  ----------------------------------------------------------------
//         N X0 Y0      solvable   max.moves   reachable states
//         4 0  0  ->      no        13             1688
//         4 1  0  ->      yes       14             1872
//         4 1  1  ->      no        13             2116
//         5 0  0  ->      no        22           873327
//         5 1  0  ->      no        22           706392
//         5 2  0  ->      yes       23          110468?
//         5 1  1  ->      no        22           466059
//         5 2  1  ->      yes       23           775304
//         5 2  2  ->      no        22          118392?
//  ----------------------------------------------------------------
//
// **************************************************************************

macro N = 4;
macro X0 = 1;
macro Y0 = 1;

macro UP = 0b00;
macro DOWN = 0b01;
macro LEFT = 0b10;
macro RIGHT = 0b11;

module Solitaire(
    bv{2} ?move,
    nat{N} x, y,
    [N][N()]bool f
) {
    // initialize the square
    for(i=0..N-1)
        for(j=0..N-1)
            if(i!=X0 | j!=Y0)
                f[i][j] = true;

    // play the game
    loop {
        if(x<N & y<N()) {
            case
            (move==UP) do {
                if(y<=N-3 & f[x][y] & f[x][y+1] & !f[x][y+2]) {
                   next(f[x][y+2]) = true;
                   next(f[x][y+1]) = false;
                   next(f[x][y])    = false;
                }
             }
             (move==DOWN) do {
                if(y>=2 & f[x][y] & f[x][y-1] & !f[x][y-2]) {
                   next(f[x][y-2]) = true;
                   next(f[x][y-1]) = false;
                   next(f[x][y])    = false;
                }
             }
             (move==LEFT) do {
                if(x>=2 & f[x][y] & f[x-1][y] & !f[x-2][y]) {
                   next(f[x-2][y]) = true;
                   next(f[x-1][y]) = false;
                   next(f[x][y])    = false;
                }
             }
             (move==RIGHT) do {
                if(x<=N-3 & f[x][y] & f[x+1][y] & !f[x+2][y]) {
                   next(f[x+2][y]) = true;
                   next(f[x+1][y]) = false;
                   next(f[x][y])    = false;
                }
             }
             default nothing;
        }
        pause;
    }
} satisfies {
    s0[DisProveA]: assert A G
        exists(i=0..N-1) exists(j=0..N()-1) exists(k=0..N-1) exists(l=0..N-1)
            (! ((k==i) & (l==j)) & f[i][j] & f[k][l]) ;
}