#include<civlc.cvh>

$input int n;

$proc procs[n];

void f(int pid) {
  for (int i=0; i<n; i++) {
    $assert($collective(procs, n) i==procs[(i+1)%n]@i );
  }
}

void main() {
  $assume(n>0);
  for (int i=0; i<n; i++) procs[i] = $spawn f(i);
  for (int i=0; i<n; i++) $wait procs[i];
}