// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// Find the first element of an array that has a certain property. In the case//
// below, the property has already been applied to form a boolean array, and  //
// thus, we seek the index of the first "true" in the array.                  //
// Note that algorithm FirstOne requires time O(1) using O(N^2) processors.   //
// The algorithm below applies FirstOne twice to reduce the number of required//
// processors to O(N) while still requiring time O(1).                        //
// ************************************************************************** //

macro M = 4;
macro N = M*M;


module FirstOneOpt([N]bool ?a,nat{N} index, event !rdy) {
    [N]bool x;
    [M]bool y;
    nat{M} yindex;

    // use O(N) processors to copy a to x; one might apply a desired property
    // to a[i] before copying, so that arbitrary properties can be checked
    for(i=0..N-1)
        x[i] = a[i];

    // use O(M^2) = O(N) processors to check in which groups of size M there
    // are true bits 
    for(i=0..M-1)
        for(j=0..M-1)
            if(x[i*M+j])
                y[i] = true;

    // apply FirstOne to determine the first index of a group holding a true bit
    // this requires O(M^2)=O(N) processors and O(1) time
    for(i=0..M-2)
        for(j=i+1..M-1)
            if(y[i] & y[j])
                next(y[j]) = false;
    w1: pause;

    // now, at most one y[i] is true; if so, i is the desired index
    for(i=0..M-1)
        if(y[i])
            yindex = i;

    // we now know that the first true bit is in x[yindex*M..yindex*M+M-1]
    // thus, apply FirstOne again to this subsequence to determine the index
    for(i=0..M-2)
        for(j=i+1..M-1)
            if(x[yindex*M+i] & x[yindex*M+j])
                next(x[yindex*M+j]) = false;
    w2: pause;

    // now, at most one x[i] in x[yindex*M..yindex*M+M-1]is true;
    // if so, this i is the desired index
    for(i=0..M-1)
        if(x[yindex*M+i])
            index = yindex*M+i;

    emit(rdy);
}
drivenby {
    for(i=0..N-1)
        a[i] = i==5 | i==7 | i==9 | i==11;
    await(rdy);
    assert(a[index] -> forall(i=0..N-1) (i<index -> !a[i]));
}