moesi(var modified, shared, exclusive, invalid, owned) {
exclusive = 0;
modified = 0;
shared = 0;
while (?) {
if (?) {
assume(invalid != 0);
shared = shared + exclusive + 1;
owned = owned + modified;
invalid = invalid - 1;
exclusive = 0;
modified = 0;
}
else if (?) {
assume(exclusive != 0);
exclusive = exclusive - 1;
modified = modified + 1;
}
else if (?) {
assume(shared != 0);
invalid = invalid + modified + exclusive
+ shared + owned - 1;
shared = 0;
exclusive = 1;
modified = 0;
owned = 0;
}
else if (?) {
assume(owned != 0);
invalid = invalid + modified + exclusive
+ shared + owned - 1;
shared = 0;
exclusive = 1;
modified = 0;
owned = 0;
}
else {
assume(invalid != 0);
invalid = invalid + modified + shared +
exclusive + owned - 1;
shared = 0;
exclusive = 1;
modified = 0;
owned = 0;
}
}
}