// ************************************************************************** // // // // 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 // // // // ************************************************************************** // // GnomeSort is a remarkable simple sorting algorithm and has been defined // // by Hamid Sarbazi-Azad in 2000 (called StupidSort at that time). The idea // // is that when looking at BubbleSort when the first swap appears, one knows // // that the subsequence to the left is already sorted. Thus, a new swap may // // only happen in the subsequence starting at the next leftmost position // // up to the right end of the sequence. Thus, the swap operations restart // // from there, so that only a single loop is required. Nevertheless, the // // algorithm has complexity O(n^2). // // ************************************************************************** // macro aSize = 16; macro iSize = 64; module GnomeSort([aSize]int{iSize} ?a,b, event ready) { nat{aSize+1} i; for(i=0..(aSize-1)) b[i] = a[i]; i = 0; weak abort loop { // an invariant is here that b[0..i] is already sorted if(b[i] > b[i+1]) { next(b[i]) = b[i+1]; next(b[i+1]) = b[i]; if(i!=0) next(i) = i-1; } else if(i==aSize-2) emit(ready); else next(i) = i+1; pause; } when(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); }