// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// ShellSort [Shel59,Cyph89,PlPS92,Sedg96,JiLV00,Ciur01] is a variant of      //
// InsertionSort. It performs InsertionSort on h-sequences b[0],b[h],b[2h],...//
// of the array b and repeats this for smaller h until h=1 (so that in this   //
// last step an InsertionSort is made). It is to be noted that a h-sorted     //
// sequence remains h-sorted when sorting by another step h' is done later.   //
// The performance of ShellSort depends on the chosen set of numbers h (see   //
// [Ciur01]), where theoretically any sequence can be used that ends with h=1.//
// Donald Shell proposed the sequence h=1,2,4,8,... which is however not      //
// that good. A better sequence is h=1,3,7,15,31,... (i.e. h_i = 2^i-1) for   //
// which Knuth proved the worst case complexity O(n^1.5) which cannot be      //
// improved due to Prat. Another often used sequence is h=1,4,13, (i.e.       //
// h_{i+1} = 3*h_i+1). Pratt proved 1971 that h=1,2,3,4,6,9,8,12,18,27,..     //
// requires only O(n*(log(n))^2) steps where the sequence is obtained         //
// by adding 2*h_i and 3*h_i to the sequence if these numbers are not already //
// at the end of the sequence (i.e., h_i = 2^j*3^k for all j,k). Using this   //
// sequence and BubbleSort instead of InsertionSort, a sorting network can be //
// built with the same complexity of Batcher's bitonic sorter.                //
// ************************************************************************** //

[16] nat a;
[3] nat steps;

function ShellSort (nat aSize, sizeStep): nat {
    nat i,j,h,s,t,v;

    steps[0] = 7;
    steps[1] = 3;
    steps[2] = 1;

    for(s=0..sizeStep-1) {
        h = steps[s];
        for(i=h..aSize-1) {
            t = a[i];
            j = i;
            v = a[j-h];
            while(j>=h & v>t) {
                a[j] = v;
                j = j-h;
                if(j>=h)
                    v = a[j-h];
            }
            a[j]=t;
	    }
    }
    return 0;
}


thread test{
    nat k;
    a[0] = 9;
    a[1] = 8;
    a[2] = 16;
    a[3] = 15;
    a[4] = 1;
    a[5] = 10;
    a[6] = 2;
    a[7] = 11;
    a[8] = 3;
    a[9] = 4;
    a[10] = 6;
    a[11] = 5;
    a[12] = 14;
    a[13] = 12;
    a[14] = 7;
    a[15] = 13;

    k = ShellSort(16,3);
}


thread test1{
    nat t,i;
    bool test1_passed;

    for(i=0..15){
        a[i]=i+1;
    }
    a[5]=9; 
    a[8]=6; 
    a[10]=7;
    a[6]=11;
    test1_passed = true;

    t = ShellSort(16,3);

    for(i=0..15){
        if((a[i]==(i+1)) & (test1_passed != false)){
            test1_passed = true;
        }else{
        test1_passed = false;
        }
    }

}

thread test2{
   nat t, i;
    bool test2_passed;

    for(i=0..15){
        a[i]=i+1;
    }
    test2_passed = true;
    t = ShellSort(16,3);

    for(i=0..15){
        if((a[i]==(i+1)) & (test2_passed != false)){
            test2_passed = true;
        }else{
        test2_passed = false;
        }
    }
}

thread test3{
    nat t, i;
    bool test3_passed;

    for(i=0..15){
        a[i]=16-i;
    }
    test3_passed = true;
    t = ShellSort(16,3);

    for(i=0..15){
        if((a[i]==(i+1)) & (test3_passed != false)){
            test3_passed = true;
        }else{
        test3_passed = false;
        }
    }

}