```// **************************************************************************
//
//    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
//
// **************************************************************************
//
//  Knight's Tour
//
//  The problem is to find a path for a Knight on a (N)x(N) chessboard,
//  such that every field is visited exactly once. It is known that
//  there is a Hamilton circuit (a Knight's Tour where start and end
//  points are identical) iff N>=6 and N is even.
//
//  A Knight's Tour can be easily obtained by divide and conquer
//  algorithms or heuristics like Warnsdorff's rule (from 1823).
//  For further references see the PDF files.
//
// **************************************************************************

macro N = 4;

module KnightsTour(
bv{3} move,
[N][N()]bool q,
nat{N} x, y
) {
x = 1;
y = 0;
always {
q[x][y] = true;
case
(move==0b000) do {
if(x>=2 & y>=1)
if(!q[x-2][y-1]) {
next(x) = x-2;
next(y) = y-1;
}
}
(move==0b001) do {
if(x>=1 & y>=2)
if(!q[x-1][y-2]) {
next(x) = x-1;
next(y) = y-2;
}
}
(move==0b010) do {
if(x<N-1 & y>=2)
if(!q[x+1][y-2]) {
next(x) = x+1;
next(y) = y-2;
}
}
(move==0b011) do {
if(x<N-2 & y>=1)
if(!q[x+2][y-1]) {
next(x) = x+2;
next(y) = y-1;
}
}
(move==0b100) do {
if(x<N-2 & y<N()-1)
if(!q[x+2][y+1]) {
next(x) = x+2;
next(y) = y+1;
}
}
(move==0b101) do {
if(x<N-1 & y<N()-2)
if(!q[x+1][y+2]) {
next(x) = x+1;
next(y) = y+2;
}
}
(move==0b110) do {
if(x>=1 & y<N-2)
if(!q[x-1][y+2]) {
next(x) = x-1;
next(y) = y+2;
}
}
(move==0b111) do {
if(x>=2 & y<N-1)
if(!q[x-2][y+1]) {
next(x) = x-2;
next(y) = y+1;
}
}
default
nothing;
}
} satisfies {
spec[DisProveA] : assert
! E F forall(i=0..N-1) forall(j=0..N()-1) q[i][j];
}
```