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