// ************************************************************************** //
//                                                                            //
//    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 file implements the well-known bubble sort procedure. The main idea   //
// is to consider all pairs (x[i-1],x[i]) in the array x[0..N-1] and to swap  //
// them whenever x[i-1] > x[i] holds. This is repeated unless no more swaps   //
// are seen in such a round (noted in variable swapped).                      //
// ************************************************************************** //

procedure BubbleSort([]nat x,nat xlen) {
    nat i,y,swapped;
    do {
        swapped = 0;
        for(i=1..xlen-1) {
            // if this pair x[i-1],x[i] is in the wrong order
            if(x[i-1] > x[i]) {
                // then swap them and remember that something changed
                y = x[i-1];
                x[i-1] = x[i];
                x[i] = y;
                swapped = 1;
            }
        }
    } while(swapped==1)
    return;
}


// create a test array in reverse order
procedure Initialize([]nat x,nat xlen) {
    nat i;
    for(i=0..xlen-1)
        x[i] = xlen-i;
    return;
}


thread t {
    [10]nat x;
    Initialize(x,10);
    BubbleSort(x,10);
}