```// ************************************************************************** //
//                                                                            //
//    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 Quartz module illustrates causality by solving Sudokus. Given//
// a Sudoku x (where the empty fields are filled by zeros), the module below  //
// copies the known values into the array y. After that, the Sudoku rules are //
// listed to make further assignments to the single fields y[i][j]. Note that //
// the entire computation is done within a single macro step, where y[i][j]   //
// may already have its final value or the unknown value ⊥. This way, known   //
// values, i.e., the "must" information propagate themselves. The "can/may"   //
// information, i.e., which values are forbidden in particular fields y[i][j] //
// is maintained in the local array p: p[i][j][v] holds if value v is possible//
// in field y[i][j].                                                          //
// ************************************************************************** //

module Sudoku([9][9]nat{10} ?x,[9][9]nat{9} y) {
[9][9][9]bool p;

// retrieve initial values
for(i=0..8)
for(j=0..8)
if(x[i][j]>0)
let(v = x[i][j]-1) {
y[i][j] = v;
p[i][j][v] = true;
}

// no value must appear twice in a group
for(i=0..8)
for(j=0..8) {
// row constraint
for(k=0..8)
if(k!=j)
p[i][k][y[i][j]] = false;
// column constraint
for(k=0..8)
if(k!=i)
p[k][j][y[i][j]] = false;
// square constraint
let(i0=3*(i/3))
let(j0=3*(j/3))
for(i1=0..2)
for(j1=0..2)
if((i0+i1!=i) | (j0+j1!=j))
p[i0+i1][j0+j1][y[i][j]] = false;
}

// assign value if this is the only possible place in a group
for(i=0..8)
for(j=0..8)
for(v=0..8) {
// unique possibility
if(!exists(k=0..8) (k!=v & p[i][j][k])) {
y[i][j] = v;
p[i][j][v] = true;
}
// row constraint
if(!exists(k=0..8) (k!=j & p[i][k][v])) {
y[i][j] = v;
p[i][j][v] = true;
}
// column constraint
if(!exists(k=0..8) (k!=i & p[k][j][v])) {
y[i][j] = v;
p[i][j][v] = true;
}
// square constraint
let(i0=3*(i/3))
let(j0=3*(j/3))
if(!exists(i1=0..2) exists(j1=0..2) ((i0+i1!=i | j0+j1!=j) & p[i0+i1][j0+j1][v])) {
y[i][j] = v;
p[i][j][v] = true;
}
}
}
drivenby {
[9][9]nat{10} solution;
x = [[0,0,3,0,0,6,0,0,5],
[0,2,1,0,8,0,4,3,0],
[0,4,0,0,0,1,0,0,7],
[0,0,0,3,6,9,0,0,1],
[9,0,7,1,0,8,6,0,4],
[8,0,0,2,7,4,0,0,0],
[3,0,0,8,0,0,0,5,0],
[0,8,5,0,9,0,7,4,0],
[2,0,0,7,0,0,3,0,0] ];
solution =
[[7,9,3,4,2,6,1,8,5],
[6,2,1,5,8,7,4,3,9],
[5,4,8,9,3,1,2,6,7],
[4,5,2,3,6,9,8,7,1],
[9,3,7,1,5,8,6,2,4],
[8,1,6,2,7,4,5,9,3],
[3,7,4,8,1,2,9,5,6],
[1,8,5,6,9,3,7,4,2],
[2,6,9,7,4,5,3,1,8] ];
for(i=0..8)
for(j=0..8)
assert(y[i][j] == solution[i][j]-1);
}
```