// ************************************************************************** //
//                                                                            //
//    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], the algorithm below determines its maximum using //
// O(N^2) processors in constant time, i.e. one macro step. To this end, all  //
// pairs of elements a[i],a[j] are considered and m[i] = true is written to a //
// local array m[0..N-1] in case a[i] < a[j] holds. Note that several writes  //
// may occur in this macro step, but all write the same value (so this is a   //
// CRCW PRAM algorithm). In a second part of the macro step, we can determine //
// the maximum in that those indices having m[i]=false are determined.        //
// ************************************************************************** //

macro N = 8;
macro R = 8;

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_O1([N]int{R} ?a, int{R} max) {
    event [N]bool m;

    // set m[i] iff some a[j] is greater than a[i]
    for(i=0..N-1)
        for(j=0..N-1)
            if(a[i] < a[j])
                m[i] = true;
    // thus, those i where m[i] is false are the indices of the maximum a[i]
    // note: there might be several such indices (containing the same value)
    for(i=0..N-1)
        if(!m[i])
            max = a[i];
}
satisfies {
    correct : assert(contains(a,max) & isArrayMax(a,max));
}
drivenby {
    for(i=0..N/2-1)
        a[i] = i;
    for(i=N/2..N-1)
        a[i] = N-1-i;
    assert(contains(a,max) & isArrayMax(a,max));
}