// ************************************************************************** // // 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 // // ************************************************************************** // // The following is a generic implementation of Sam Lloyd's 15 puzzle. // The problem of SIZE=4 is given by the following matrix of numbers // // ---------------- // | 0 1 2 3 // ---------------- // 0 | 01 02 03 04 // 1 | 05 06 07 08 // 2 | 09 10 11 12 // 3 | 13 14 15 00 // ---------------- // // The field is organized in a two-dimensonal array, where the first // and second index corresponds with the rows and columns, respectively, // counted from the upper left corner as shown above. // // The task is to generate one of the following reversed matrices with // as few steps as possible: // // ---------------- ---------------- // | 0 1 2 3 | 0 1 2 3 // ---------------- ---------------- // 0 | 15 14 13 12 0 | 00 15 14 13 // 1 | 11 10 09 08 1 | 12 11 10 09 // 2 | 07 06 05 04 2 | 08 07 06 05 // 3 | 03 02 01 00 3 | 04 03 02 01 // ---------------- ---------------- // // For even SIZEs, we want to generate the left hand side matix // since the right hand side one is not reachable, and for odd // SIZEs, we want to generate the right hand side matix // since the left hand side one is not reachable. // // Henry Ernest Dudeney posed the question for SIZE=3 and required // 36 moves for his answer. Martin Gardner asked readers of the // "Scientific American" magazine to solve the puzzle in less steps. // SMV generated the solution with 30 moves, which is optimal. // Moreover, SMV counts 181441 reachable states. // // ************************************************************************** macro SIZE=4; macro up = !m1 & !m0; macro down = !m1 & m0; macro left = m1& ! m0; macro right = m1 & m0; macro EVEN(x) = ((x/2)*2 == x); module Lloyd15( bool ?m1, ?m0, [SIZE][SIZE]nat{SIZE*SIZE+1} field, nat{SIZE} hole_x, hole_y, event !nowin, event !Right,!Left,!Up,!Down ) { // define the initial configuration hole_x = SIZE-1; hole_y = SIZE-1; for(row=0..SIZE-1) for(col=0..SIZE-1) if( row==(SIZE-1) & col==(SIZE-1) ) field[row][col] = 0; else field[row][col] = (row*SIZE)+col+1; // searching a solution by random inputs loop { if (right) { emit (Right); if (hole_y!=SIZE-1) { next(field[hole_x][hole_y]) = field[hole_x][hole_y+1]; next(field[hole_x][hole_y+1]) = field[hole_x][hole_y]; next(hole_y) = hole_y+1; } } else if (left) { emit (Left); if (hole_y!=0) { next(field[hole_x][hole_y]) = field[hole_x][hole_y-1]; next(field[hole_x][hole_y-1]) = field[hole_x][hole_y]; next(hole_y) = hole_y-1; } } else if (up) { emit (Up); if (hole_x!=0) { next(field[hole_x][hole_y]) = field[hole_x-1][hole_y]; next(field[hole_x-1][hole_y]) = field[hole_x][hole_y]; next(hole_x) = hole_x-1; } } else { emit (Down); if (hole_x!=SIZE-1) { next(field[hole_x][hole_y]) = field[hole_x+1][hole_y]; next(field[hole_x+1][hole_y]) = field[hole_x][hole_y]; next(hole_x) = hole_x+1; } } // check whether the desired configuration is found for (row=0..SIZE-1) for (col=0..SIZE-1) if(EVEN(SIZE)) { // even SIZE should have 0 in lower right corner // otherwise, there is no solution if(row==0 & col==0) { if(field[row][col] != 0) emit (nowin); } else if( field[row][col] != (SIZE*SIZE) - ((row*SIZE)+col) ) emit (nowin); } else { // odd SIZE should have 0u in upper left corner // otherwise, there is no solution if(row==(SIZE-1) & col==(SIZE-1)) { if(field[row][col] != 0) emit(nowin); } else if(field[row][col] != (SIZE*SIZE) - ((row*SIZE)+col+1)) emit (nowin); } pause; } } satisfies { neverwin[DisProveA] : assert A G nowin; }