bubble_sort

#define SIZE 8

int arr[SIZE];
int i;
int j;
bool wasPermutation;
int randomValue;
int tmp;
bool sortingFinished;

// generate random in range [minV, maxV]
inline genRandom(minV, maxV) {
	randomValue = minV;
	do
	:: (randomValue == maxV) -> break;	// increased up to max value => stop
	:: else					 ->
		if
		:: select(tmp : 5 .. 15);
		   randomValue = randomValue + tmp; // randomly increment
		:: select(tmp : 1 .. 100);
		   randomValue = randomValue - tmp; // randomly decrement
		:: break;			                // or stop
		fi;
	od;
	return randomValue;
}

inline swap(i1, i2) {
    tmp = arr[i1];
    arr[i1] = arr[i2];
    arr[i2] = tmp;
}

active proctype Main() {
    // fill initial array
    for (i : 0..(SIZE-1)) {
        arr[i] = genRandom(0, 100);
    }
    printf("Generated array: [");
    for (i : 0..(SIZE-1)) {
        printf("%d ", arr[i]);
    }
    printf("]\n");

    printf("Start sorting...\n");
    wasPermutation = true;
    sortingFinished = false;
    do
    :: (wasPermutation) ->
        wasPermutation = false;
        for (j : 0..(SIZE-2)) {
            if
            :: (arr[j] > arr[j+1]) ->
                swap(j, j+1);
                wasPermutation = true;
            :: else				   -> skip;
            fi;
        }
    :: else 		    ->	break;
    od;
    sortingFinished = true;

    printf("Sorted array: [");
    for (i : 0..(SIZE-1)) {
        printf("%d ", arr[i]);
    }
    printf("]\n");
}