/* CIVL model of dotproduct1.c.
 * How to verify: civl verify dotproduct1.cvl
 *
 * Limitations: bound is placed on number of threads; each thread always
 * executes iterations in increasing order; assumes a round-robin distribution
 * of iterations to threads
 */
#include <civlc.h>
#include <stdio.h>
#include <assert.h>
#define THREAD_MAX 4
/* Does thread t own iteration i in loop with n iterations? */
#define CIVL_owns(t, n, i) ((i)%(n)==(t))


void main() {
  int i, n;
  float a[8], b[8], sum;
  
  n=8;
  for (i=0; i < n; i++)
    a[i] = b[i] = i * 1.0;
  sum = 0.0;
  
  /* Translation of omp for loop: */
  {
    int nthreads = 1+$choose_int(THREAD_MAX);
    $proc threads[nthreads];
    void loop(int tid) {
      float _sum = 0.0;

      for (int i=0; i<n; i++) {
	if (CIVL_owns(tid, nthreads, i)) {
	  _sum = _sum + (a[i] * b[i]);
	  printf("loop %d\n", i);
	}
      }
      sum += _sum;
    }

    printf("nthreads = %d\n", nthreads); // for debugging
    for (int tid=0; tid<nthreads; tid++)
      threads[tid] = $spawn loop(tid);
    for (int tid=0; tid<nthreads; tid++)
      $wait(threads[tid]);
  } /* End of omp for loop */

  printf("   Sum = %f\n", sum);
  assert(sum == 140.0); // for checking correctness
}