// ************************************************************************** //
//                                                                            //
//    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 D = 3;     // digit set is -D,...,-1,0,1,...,D
macro B = 5;     // base of the radix numbers
macro N = 4;     // number of digits used for the addition

module TestSgn2IntPrinciple([N]int{D+1} ?x,[N+1]nat{B} y) {
    loop {
        pause;
        Sgn2IntPrinciple(x,y);
    }
}
drivenby {
    [N]bool skip;
    do {
        skip[0] = x[0]==D;
        skip[1] = x[1]==D & skip[0];
        skip[2] = x[2]==D & skip[1];
        skip[3] = x[3]==D & skip[2];
        next(x[0]) = (x[0]+1) % (D+1);
        next(x[1]) = (skip[0] ? (x[1]+1) % (D+1) : x[1]);
        next(x[2]) = (skip[1] ? (x[2]+1) % (D+1) : x[2]);
        next(x[3]) = (skip[2] ? (x[3]+1) % (D+1) : x[3]);
        pause;
    } while(!(forall(i=0..N-1) (x[i]==D) ));
}