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