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;
}
}
}