illinois(var dirty, shared, exclusive, invalid) {
exclusive = 0;
dirty = 0;
shared = 0;
while (?) {
if (?) {
assume(dirty == 0 && shared == 0
&& exclusive == 0);
assume(invalid != 0);
invalid = invalid - 1;
exclusive = exclusive + 1;
}
else if (?) {
assume(invalid != 0);
assume(dirty != 0);
invalid = invalid - 1;
dirty = dirty - 1;
shared = shared + 2;
}
else if (?) {
assume(invalid != 0);
assume(shared != 0);
invalid = invalid - 1;
shared = shared + exclusive + 1;
exclusive = 0;
}
else if (?) {
assume(invalid != 0);
assume(exclusive != 0);
invalid = invalid - 1;
shared = shared + exclusive + 1;
exclusive = 0;
}
else if (?) {
assume(exclusive != 0);
exclusive = exclusive - 1;
dirty = dirty + 1;
}
else if (?) {
assume(shared != 0);
invalid = invalid + shared - 1;
dirty = dirty + 1;
shared = 0;
}
else if (?) {
assume(invalid != 0);
invalid = invalid + exclusive + dirty +
shared - 1;
exclusive = 0;
shared = 0;
dirty = 1;
}
else if (?) {
assume(dirty != 0);
dirty = dirty - 1;
invalid = invalid + 1;
}
else if (?) {
assume(shared != 0);
shared = shared - 1;
invalid = invalid + 1;
}
else {
assume(exclusive != 0);
exclusive = exclusive - 1;
invalid = invalid + 1;
}
}
}