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

package latex.QuartzLRM.Experiments.Arithmetic;
import examples.Algorithms.Arithmetic.SignedDigit.*;

macro B = 4;    // base of the radix numbers
macro M = 4;    // number of digits used for x
macro N = 4;    // number of digits used for y

module TestSgnLes([M]nat{B} ?x,[N]nat{B} ?y,bool ls) {
loop {
SgnLes(x,y,ls);
pause;
}
}
drivenby {
[M+N]bool skip;
do {
skip[0] = x[0]==B-1;
skip[1] = x[1]==B-1 & skip[0];
skip[2] = x[2]==B-1 & skip[1];
skip[3] = x[3]==B-1 & skip[2];
skip[4] = y[0]==B-1 & skip[3];
skip[5] = y[1]==B-1 & skip[4];
skip[6] = y[2]==B-1 & skip[5];
skip[7] = y[3]==B-1 & skip[6];
next(x[0]) = (x[0]+1) % B;
next(x[1]) = (skip[0] ? (x[1]+1) % B : x[1]);
next(x[2]) = (skip[1] ? (x[2]+1) % B : x[2]);
next(x[3]) = (skip[2] ? (x[3]+1) % B : x[3]);
next(y[0]) = (skip[3] ? (y[0]+1) % B : y[0]);
next(y[1]) = (skip[4] ? (y[1]+1) % B : y[1]);
next(y[2]) = (skip[5] ? (y[2]+1) % B : y[2]);
next(y[3]) = (skip[6] ? (y[3]+1) % B : y[3]);
pause;
} while(!(forall(i=0..M-1) (x[i]==B-1) & forall(j=0..N-1) (y[j]==B-1)));
}
```