// ************************************************************************** // // // // 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); }