// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// SelectionSort determines in iteration i the the minimum b[imin] of the     //
// still unsorted array b[i..aSize-1]. After this, b[i] and b[imin] are       //
// swapped, so that b[0..i] is then already sorted, and the procedure is      //
// repeated for searching the minimum of b[i+1..aSize-1] until the entire     //
// array is sorted. Clearly, a variant is to search the maximum and put it    //
// on the rightmost border of the then unsorted left part.                    //
// ************************************************************************** //

macro aSize = 16;
macro iSize = 64;

module SelectionSort([aSize]int{iSize} ?a,b, event !ready) {
    nat{aSize} imin;
    for(i=0..(aSize-1))
        b[i] = a[i];
    for(i=0..(aSize-1)) {
        // find the minimum b[imin] of b[i..aSize-1]
        imin = i;
        for(j=i+1..(aSize-1)) {
            if(b[j] < b[imin])
                next(imin) = j;
            pause;
            // here, b[imin] is the minimum of b[i..j]
            assert(forall(k=i..j) (b[imin]<=b[k]));
        }
        // swap b[i] with b[imin]
        next(b[i]) = b[imin];
        next(b[imin]) = b[i];
        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);
}