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