// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// Given an array a[0..N-1], this algorithm finds its minimum and maximum in  //
// time O(N) using O(1) processors. It is nevertheless remarkable since it    //
// only requires 3*ceil(n/2) comparisons instead of 2*n-2. Note that the size //
// of the array has to be an even number.                                     //
// ************************************************************************** //

macro N =  8;
macro R = 16;
macro isArrayMax(a,x)   = forall(i=0..N-1) (a[i] <= x);
macro isArrayMin(a,x)   = forall(i=0..N-1) (a[i] >= x);
macro contains(a,x)     = exists(i=0..N-1) (a[i] == x);


module Maximum_ON([N]int{R} ?a,int{R} min,max, event !rdy) {
    int{R} lmin, lmax;
    nat{N+1} i;

    assume((N/2)*2==N);
    i = 0;
    min = a[N-1];
    max = a[N-1];

    while(i<N-1) {
        // compute local minimum and maximum of a[i] and a[i+1]
        if(a[i] <= a[i+1]) {
            lmin = a[i];
            lmax = a[i+1];
        } else {
            lmin = a[i+1];
            lmax = a[i];
        }
        // and "combine" it with the so far computed min and max
        if(lmin<min)
            next(min) = lmin;
        if(lmax>max)
            next(max) = lmax;
        next(i) = i+2;
        w: pause;
    }
    emit(rdy);
    assert(contains(a,max) & isArrayMax(a,max));
    assert(contains(a,min) & isArrayMin(a,min));
}
drivenby {
    for(i=0..(N-1)/2-1)
        a[i] = i;
    for(i=(N-1)/2..N-1)
        a[i] = N-i;
    dw: await(rdy);
    assert(contains(a,max) & isArrayMax(a,max));
}