source: CIVL/examples/collective.cvl@ 844ebd8

\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];
}