// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// InsertionSort has in iteration i the array b[0..i] already sorted, and     //
// will insert b[i+1] (it could be any other value of the unsorted part as    //
// well) in b[0..i]. To this end, it right shifts all elements b[j..i] that   //
// are greater than b[i+1] and inserts b[i+1] at b[j].                        //
// ************************************************************************** //

macro aSize = 16;
macro iSize = 64;

module InsertionSort([aSize]int{iSize} ?a,b, event !ready) {
    nat{aSize+1} j;
    nat{iSize} val;
    for(i=0..aSize-1)
        b[i] = a[i];
    for(i=1..aSize-1) {
        val = b[i];
        j = i-1;
        while(b[j]>val & j>0) {
            next(b[j+1]) = b[j];
            next(j) = j-1;
            pause;
        }
        if(b[j]>val) {
            assert(j==0);
            next(b[1]) = b[0];
            next(b[0]) = val;
        } else {
            assert(b[j]<=val);
            next(b[j+1]) = val;
        }
        pause;
        // an invariant is here that b[0..i] is already sorted
        assert(forall(k=1..i) (b[k-1]<=b[k]));
    }
    emit(ready);
}
drivenby Test01 {
    for(i=0..aSize-1) a[i] = i;
    dw: await(ready);
    for(i=0..aSize-1) assert(b[i] == i);
}
drivenby Test02 {
    for(i=0..aSize-1) a[i] = aSize-1-i;
    dw: await(ready);
    for(i=0..aSize-1) assert(b[i] == i);
}
drivenby Test03 {
    for(i=0..aSize-1)
        a[i] = ((i%2==0)?i:((aSize%2==0)?aSize-i:aSize-1-i));
    dw: await(ready);
    for(i=0..aSize-1) assert(b[i] == i);
}