// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// The following implements a simple linear search algorithm that scans a     //
// given array from left to right while searching for a desired value v. The  //
// algorithm will always terminate. In case v is contained in the array, we   //
// have a[i]==v at termination time, otherwise a[i]!=v and i=N-1. Note that   //
// there will be never an out-of-bound access to the array.                   //
// ************************************************************************** //

macro N = 16;
macro M = 64;
macro contains(a,x) = exists(i=0..N-1) (a[i] == x);


module Search_ON([N]int{M} ?a,int{M} ?v,nat{N} i,event !rdy) {

    i = 0;
    while(a[i]!=v & i<N-1) {
        next(i) = i+1;
        pause;
    }
    emit(rdy);
    assert(contains(a,v) -> a[i] == v);
}
drivenby {
    v = 8;
    for(i=0..N-1)
        a[i] = 2*i;
    await(rdy);
}
drivenby {
    v = 15;
    for(i=0..N-1)
        a[i] = 2*i;
    await(rdy);
}