source: CIVL/examples/languageFeatures/atomStatement.cvl@ ac43965

/* Commandline execution:
 *              civl verify atomStatement.cvl
 * */
#include<civlc.cvh>
int n = 3;
void foo(){
  int k = n;
  k = k + 1;
}

void main(){
  int i = 0;
  int x = 3;
  $proc procs[5];
        
  $atom {
    if(i < 0)
          i = 1;
    else 
          i = 2;
  }
  $assert(i == 2);
  $atom
    if(i > 0)
      i = 1;
        else 
          i = 2;
  $assert(i == 1);
  $atom {
    i = 2;
        switch(i) {
          case 1: i = 2;
          case 2: i = 3;break;
          default: i = 5;
        }
  }
  $assert(i == 3);
  $atom {
    i = 0;
    for(int j = 0; j < 10; j++) {
      i += j;
    }
  }
  $assert(i == 45);
  $atom {
    for(int m = 0; m < 5; m++) {
      procs[m] = $spawn foo();
        }
  }
  //nested atomic and non-pure-local atomic block
  $atom {
    n = 0;
    n += 1;
    $atom {
      i+=2;
      i += 3; 
    }
    n += 9;
  }
  $assert(n == 10);
  for(int m = 0; m < 5; m++) {
    $wait(procs[m]);
  }
}