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