source: CIVL/mods/dev.civl.com/examples/concurrency/civl172miss.cvl@ cb4d4f4

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

int proc(int pid) {
 L1:  y = $choose_int(2);
  $atomic{
    y++;
    $assert(pid != 0 || y != 3);
  }
  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;
}