source: CIVL/examples/concurrency/locksBad.cvl@ bfebb46

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

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

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

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