chan msgs = [4] of { bit };
int count = 0;

active [1] proctype Producer() { // one producer
  do :: atomic { count++; msgs ! 1; } od
}

active [4] proctype Consumer() { // four consumers
  do :: atomic { msgs ? 1 -> count--; } od
}

ltl always_positive { always (count >= 0) }