// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// This is the well-known binary search algorithm that expects a sorted array //
// and a value whose membership in the array is to be checked. The algorithm  //
// starts looking at the entire array a[left..right] with left=0 and right=N-1//
// and compares the middle element a[mid] with v. Since the array is sorted,  //
// the algorithm next proceeds inspecting either the lower half a[left..mid]  //
// or the upper half a[mid+1..right] of the array.                            //
// It is well-known that most binary search algorithms are broken in that the //
// computation of mid suffers from arithmetic overflows. This does not happen //
// in Quartz since the arithmetic operations are performed in full precision. //
// ************************************************************************** //

macro N = 16;
macro M = 62;

macro sorted(a)     = forall(i=0..N-2) (a[i] <= a[i+1]);
macro contains(a,x) = exists(i=0..N-1) (a[i] == x);
macro compare(a,b)  = forall(i=0..N-1) (a[i] == b[i]);


module Search_OlogN([N]int{M} ?a,int{M} ?v,nat{N} i,event !rdy) {
    nat{N} left,right,mid;
    assume(sorted(a));
    left  = 0;
    right = N-1;
    do {
        mid = (left+right)/2;
        if(v <= a[mid])
            next(right) = mid;
        else
            next(left) = mid+1;
        pause;
    } while(left<right);
    i = left;
    emit(rdy);
    assert(contains(a,v) -> a[i] == v);
}
satisfies {
    termination : assert A F rdy;
}
drivenby {
    v = 2;
    for(i=0..N-1)
        a[i] = 2*i;
    await(rdy);
}