source: CIVL/examples/fairness/fair2.cvl

/* This program has a non-terminating fair execution */
#include <stdio.h>

int l1=0, l2=0;

void f() {
  while (1) {
    $when (l2==0) l2=1;
    printf("bye\n");
    l2=0;
  }
}

int main() {
  $proc p1 = $spawn f();
  $when (l1==0) l1=1;
  printf("hi\n");
  l1=0;
  $wait(p1);
}