// ============================================================================
// Name:        Partition
// Description: Let a[0..n-1] be an array of numbers with x = a[0]. Permute the
//              elements and set the index p such that the following holds:
//              - a[i] <= x for 0 <= i < p
//              - a[p] = x
//              - a[i] > x for p < i < n
// References:  D. Gries. The Science of Programming. Springer, 1981.
// Parameters:  SIZE (size of array)
//              INFINITE (use variables with infinite bit width)
//              BITS (bit width for finite variables)
// ============================================================================

#ifndef SIZE
#define SIZE 4u
#endif

#ifdef INFINITE
#define TYPE int
#else
#ifndef BITS
#define BITS 4u
#endif
#define TYPE int[BITS]
#endif

module Partition(TYPE b[SIZE], &a[SIZE], &x, nat[sizeOf(SIZE)] &p, &q, event &ready, &fault)
   implements PartitionSpec(ready, fault) {
   sequence(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u))
      a[i] = b[i];

   x = a[0u];
   q = 1u;
   p = SIZE-1u;

   while(q <= p) {
      if(a[q] <= x)
         next(q) = q+1u;
      else
         if(a[p] > x)
            next(p) = p-1u;
         else {
            next(a[q]) = a[p];
            next(a[p]) = a[q];
            next(q) = q+1u;
            next(p) = p-1u;
         }
      pause;
   }

   if(p > 0) {
      next(a[0u]) = a[p];
      next(a[p]) = a[0u];
   }
   pause;

   emit ready;
   CheckSpec(a, x, p, q, fault);
}

module CheckSpec(TYPE &a[SIZE], &x, nat[sizeOf(SIZE)] &p, &q, event &fault) {
   q = 0u;
   while(q < p) {
      if(a[q] > x)
         emit fault;
      next(q) = q+1u;
      pause;
   }
   if(a[q] != x)
      emit fault;
   next(q) = q+1u;
   pause;
   while(q < SIZE) {
      if(a[q] <= x)
         emit fault;
      next(q) = q+1u;
      pause;
   }
}

spec PartitionSpec(event ready, fault) {
   termination: A F ready;
   correctness: A G !fault;
}