#include<civlc.cvh>
$input int N=3;
int y = 0;

int proc(int pid) {
 L1:  y = $choose_int(2); 
  $atomic{ 
    y++;
    $assert(y!=N+1);
  }
  goto L1;
  return 0;
}

int main() {
  $proc procs[N];  
  
  $atomic{ 
    for (int i = 0; i < N; i++)
      procs[i] = $spawn proc(i);
  }
  for (int i = 0; i < N; i++)
    $wait(procs[i]);  
  return 0;
}