/* Commandline execution:
 * 		civl verify locksGood.cvl
 * */
_Bool lock0 = 0;
_Bool lock1 = 0;

void proc0() {
  $atomic {
    while (1) {
      $when (!lock0) lock0=1;
      $when (!lock1) lock1=1;
      lock0=0;
      lock1=0;
    }
  }
}

void proc1() {
  $atomic {
    while (1) {
      $when (!lock0) lock0=1;
      $when (!lock1) lock1=1;
      lock0=0;
      lock1=0;
    }
  }
}

void main() {
  $spawn proc0();
  $spawn proc1();
}