// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // ShakerSort is a symmetric version of BubbleSort. BubbleSort has the // // disadvantage that small elements on the right of the sequence move // // slowly towards the left (thus they are called turtles), while large // // elements on the left move rapidly to the right (thus they are called // // rabbits). ShakerSort therefore first bubbles the maximum of the // // still unsorted sequence to the right, and then the minimum to the left. // // ************************************************************************** // macro aSize = 16; macro iSize = 64; module ShakerSort([aSize]int{iSize} ?a,b, event !ready) { nat{aSize+1} i,j; bool swapped; event sorted; for(i=0..(aSize-1)) b[i] = a[i]; i = 0; j = 1; weak abort { loop { next(swapped) = false; w0: pause; // bubbling up the max. of b[i..N-(i+1)] j = i; while(j<aSize-(i+2)) { if(b[j] > b[j+1]) { next(b[j]) = b[j+1]; next(b[j+1]) = b[j]; next(swapped) = true; } next(j) = j+1; w1: pause; } if(b[j] > b[j+1]) { next(b[j]) = b[j+1]; next(b[j+1]) = b[j]; next(swapped) = true; } w2: pause; next(swapped) = false; if(!swapped) emit(sorted); assert(j==aSize-(i+2)); next(j) = j-1; w3: pause; // now, b[N-(i+1)] is the max of b[i..N-(i+1)], thus // bubbling down the min. of b[i..N-(i+2)] while(j>i) { if(b[j] > b[j+1]) { next(b[j]) = b[j+1]; next(b[j+1]) = b[j]; next(swapped) = true; } next(j) = j-1; w4: pause; } if(b[j] > b[j+1]) { next(b[j]) = b[j+1]; next(b[j+1]) = b[j]; next(swapped) = true; } w5: pause; next(i) = i+1; next(swapped) = false; if(!swapped) emit(sorted); } } when(sorted); 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); }