source: CIVL/examples/languageFeatures/atomicWait.cvl@ dfb0fef

/* Commandline execution:
 *              civl verify -inputN=3 atomicWait.cvl
 * */
#include <civlc.cvh>
$input int N;
int sum = 0;

void foo(int i){
  sum += i;
}

void main(){
  $atomic{
    $proc ps[N];
    for(int j = 1; j < N+1; j ++){
      ps[j-1] = $spawn foo(j);
    }
    for(int j = 1; j < N+1; j ++){
      $wait(ps[j-1]);
    }
  }
  $assert(sum == N*(N+1)/2);
}