// ************************************************************************** //
//                                                                            //
//    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 parallel prefix problem (also known a list ranking see [KaRa88]) is    //
// defined as follows: For an array x[0..N-1], we have to compute the values  //
// y[i] = sum(j=0..i) x[j] for all i=0..N-1. The module below computes these  //
// values in log(N) time using O(N) processors which is an optimal PRAM       //
// algorithm.                                                                 //
// The version below is due to Andrews. Concurrent Programming - Principles   //
// and Practice. The Benjamin/Cummings Publishing Company, 1991.              //
// ************************************************************************** //

macro N =  8;


module ListRanking3([N]int ?x,y,event !rdy) {
    nat{2*(N-1)} d;

    for(i=0..N-1)
        y[i] = x[i];

    d = 1;
    while(d<N) {
        for(i=0..N-1)
            if(i>=d)
                next(y[i]) = y[i-d]+y[i];
        next(d) = d+d;
        pause;
    }
    emit(rdy);
    assert(forall(i=0..N-1) (y[i] == sum(j=0..i) x[j]));
}
satisfies {
    termination: assert A F rdy;
}
drivenby {
    for(i=0..N/2-1)
        x[i] = i;
    for(i=N/2..N-1)
        x[i] = N-1-i;
    await(rdy);
}