/**
 * Test me: abc -iquote examples/link/barrier examples/link/barrier/barrier.cvl examples/link/barrier/concurrency.cvl
 */
 
#include<civlc.cvh>
#include<concurrency.cvh>
 
$input int N;
$input int B;
$assume(N > 0 && N < B);
$gbarrier gbarrier = $gbarrier_create($here, N);
int counter = 0;
 
void process(int id) {
  $barrier barrier = $barrier_create($here, gbarrier, id);

  while($true){
    $assert((counter == 0));
    $barrier_call(barrier);
    counter++;
    $barrier_call(barrier);
    $assert((counter == N));
    $barrier_call(barrier);
    counter--;
    $barrier_call(barrier);
  }
  $barrier_destroy(barrier);
}
 
void main(){
  $proc procs[N];
  
  for(int i = 0; i < N; i++)
    procs[i] = $spawn process(i);
  for(int i = 0; i < N; i++)
    $wait(procs[i]);
  $gbarrier_destroy(gbarrier);
}