```// ************************************************************************** //
//                                                                            //
//    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);
}
```