// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// BubbleSort first performs the following compare/swap operations on an      //
// array b: (0,1); (1,2); (2,3); ..., (n-2,n-1). Then, the maximal element    //
// is at the rightmost position b[n-1]. After this, in round i, the swap      //
// operations (0,1); (1,2); (2,3); ..., (n-i-1,n-i) are performed, so         //
// that b[n-i..n-1] contains already the final elements.                      //
// The algorithm below already makes use of an optimization in that it is     //
// stored whether a swap operation has been performed on b[0..n-i-1]. If      //
// not, then also this part is already sorted, and thus, the algorithm        //
// terminates.                                                                //
// ************************************************************************** //

macro aSize = 16;
macro iSize = 64;

module BubbleSortOpt([aSize]int{iSize} ?a,b, event !ready) {
    nat{aSize+1} i,j;
    bool swapped;
    for(i=0..(aSize-1))
        b[i] = a[i];
    i = 0;
    j = 1;
    do {
        next(swapped) = false;
        next(i) = i+1;
        w0: pause;
        j = 1;
        while(j<aSize-i) {
            if(b[j-1] > b[j]) {
                next(b[j]) = b[j-1];
                next(b[j-1]) = b[j];
                next(swapped) = true;
            }
            next(j) = j+1;
            w1: pause;
        }
        if(b[j-1] > b[j]) {
            next(b[j]) = b[j-1];
            next(b[j-1]) = b[j];
            next(swapped) = true;
        }
        w2: pause;
    } while(swapped);
    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);
}