#include<civlc.h>

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