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

```