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