berkeley(var unowned, exclusive, nonexclusive, invalid) {

  unowned = 0;
  exclusive = 0;
  nonexclusive = 0;

  while (?) {

    if (?) {
      assume(invalid != 0);

      nonexclusive = nonexclusive + exclusive;
      unowned = unowned + 1;
      invalid = invalid - 1;
      exclusive = 0;    
    }
    else if (?) {
      assume(invalid != 0);

      invalid = invalid + exclusive + nonexclusive + unowned - 1;
      exclusive = 1;
      nonexclusive = 0;
      unowned = 0;
    }
    else if (?) {
      assume(nonexclusive != 0);

      invalid = invalid + nonexclusive + unowned - 1;
      exclusive = exclusive + 1;
      nonexclusive = 0;
      unowned = 0;
    }
    else {
      assume(unowned != 0);

      invalid = invalid + nonexclusive + unowned - 1;
      exclusive = exclusive + 1;
      nonexclusive = 0;
      unowned = 0;
    }
  }
}