Repair/RepairCompiler/MCC/IR/GraphAnalysis.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import java.io.*;
   4 import MCC.State;
   5 import MCC.Compiler;
   6
   7 public class GraphAnalysis {
   8     Termination termination;
   9     static final int WORKS=0;
  10     static final int ERR_NOREPAIR=1;
  11     static final int ERR_CYCLE=2;
  12     static final int ERR_RULE=3;
  13     static final int ERR_ABSTRACT=4;
  14
  15     public GraphAnalysis(Termination t) {
  16         termination=t;
  17     }
  18
  19     private boolean safetransclosure(GraphNode gn, Set removed, Set cantremove, Set couldremove) {
  20         Stack workset=new Stack();
  21         HashSet closureset=new HashSet();
  22         boolean needcyclecheck=false;
  23         HashSet cantremovetrans=new HashSet();
  24         workset.push(gn);
  25         while(!workset.empty()) {
  26             GraphNode gn2=(GraphNode)workset.pop();
  27             if (!closureset.contains(gn2)) {
  28                 closureset.add(gn2);
  29                 boolean goodoption=false;
  30                 for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
  31                     GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
  32                     if (removed.contains(gn3))
  33                         continue;
  34                     if (((cantremove.contains(gn2)||!couldremove.contains(gn2))
  35                          &&termination.conjunctions.contains(gn2))||
  36                         cantremovetrans.contains(gn2))
  37                         cantremovetrans.add(gn3);
  38
  39                     if (termination.abstractrepair.contains(gn3)||
  40                         termination.conjunctions.contains(gn3)||
  41                         termination.updatenodes.contains(gn3)) {
  42                         /**  Check for cycles if the graphnode can't
  43                          * be removed (we know we aren't introducing
  44                          * new things to repair). */
  45                         if ((!termination.abstractrepair.contains(gn3)&&
  46                              cantremove.contains(gn3))||
  47                             cantremovetrans.contains(gn3)) {
  48                             needcyclecheck=true;
  49                         } else return false;
  50                     }
  51                     if ((!couldremove.contains(gn3))||cantremove.contains(gn3))
  52                         goodoption=true;
  53                     workset.push(gn3);
  54                 }
  55                 if (!goodoption) {
  56                     if (termination.scopenodes.contains(gn2))
  57                         return false;
  58                 }
  59             }
  60         }
  61         if (needcyclecheck) {
  62             Set cycles=GraphNode.findcycles(closureset);
  63             for(Iterator it=cycles.iterator();it.hasNext();) {
  64                 GraphNode gn2=(GraphNode)it.next();
  65                 if (termination.abstractrepair.contains(gn2)||
  66                     termination.conjunctions.contains(gn2)||
  67                     termination.updatenodes.contains(gn2))
  68                     return false;
  69             }
  70         }
  71         return true;
  72     }
  73
  74     public Set doAnalysis() {
  75         HashSet cantremove=new HashSet();
  76         HashSet mustremove=new HashSet();
  77
  78         cantremove.addAll(termination.scopenodes);
  79         cantremove.addAll(termination.abstractrepair);
  80
  81         while(true) {
  82             boolean change=false;
  83             HashSet nodes=new HashSet();
  84             nodes.addAll(termination.conjunctions);
  85             nodes.removeAll(mustremove);
  86             GraphNode.computeclosure(nodes,mustremove);
  87             Set cycles=GraphNode.findcycles(nodes);
  88             Set couldremove=new HashSet();
  89             couldremove.addAll(termination.conjunctions);
  90             couldremove.addAll(termination.updatenodes);
  91             couldremove.addAll(termination.consequencenodes);
  92             couldremove.retainAll(nodes);
  93
  94
  95             /* Check for consequence nodes which are fine */
  96
  97             for(Iterator it=termination.consequencenodes.iterator();it.hasNext();) {
  98                 GraphNode gn=(GraphNode) it.next();
  99                 if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
 100                             couldremove.remove(gn);
 101                 }
 102             }
 103
 104             /* Check for update nodes which are fine */
 105
 106             for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
 107                 GraphNode gn=(GraphNode) it.next();
 108                 if (safetransclosure(gn, mustremove,cantremove, cantremove)) {
 109                         couldremove.remove(gn);
 110                 }
 111             }
 112
 113             /* Check for conjunction nodes which are fine */
 114
 115             for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 116                 GraphNode gn=(GraphNode) it.next();
 117                 if (mustremove.contains(gn)||cantremove.contains(gn))
 118                     continue;
 119                 if (!safetransclosure(gn, mustremove,cantremove, cantremove))
 120                     continue;
 121
 122                 boolean allgood=true;
 123                 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 124                     GraphNode gn2=((GraphNode.Edge)edgeit.next()).getTarget();
 125                     TermNode tn2=(TermNode)gn2.getOwner();
 126                     assert tn2.getType()==TermNode.ABSTRACT;
 127                     boolean foundupdate=false;
 128                     for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 129                         GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();
 130                         if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
 131                             TermNode tn3=(TermNode)gn3.getOwner();
 132                             if (tn3.getType()==TermNode.UPDATE)
 133                                 foundupdate=true;
 134                         }
 135                     }
 136                     if (!foundupdate)
 137                         allgood=false;
 138                 }
 139                 if (allgood) {
 140                     couldremove.remove(gn);
 141                     if (Compiler.PRUNEQUANTIFIERS) {
 142                         TermNode tn=(TermNode)gn.getOwner();
 143                         Constraint constr=tn.getConstraint();
 144                         for(Iterator consit=((Set)termination.conjunctionmap.get(constr)).iterator();consit.hasNext();) {
 145                             GraphNode gn4=(GraphNode)consit.next();
 146                             TermNode tn4=(TermNode)gn4.getOwner();
 147                             if (tn4.getquantifiernode()) {
 148                                 mustremove.add(gn4); /* This node is history */
 149                                 System.out.println("Eliminating: "+gn4.getTextLabel());
 150                             }
 151                         }
 152                     }
 153                 }
 154             }
 155
 156
 157             /* Look for constraints which can only be satisfied one way */
 158
 159             Vector constraints=termination.state.vConstraints;
 160             for(int i=0;i<constraints.size();i++) {
 161                 Constraint c=(Constraint)constraints.get(i);
 162                 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
 163                 HashSet tmpset=new HashSet();
 164                 tmpset.addAll(conjunctionset);
 165                 tmpset.removeAll(mustremove);
 166                 if (tmpset.size()==1) {
 167                     int oldsize=cantremove.size();
 168                     cantremove.addAll(tmpset);
 169                     if (cantremove.size()!=oldsize)
 170                         change=true;
 171                 }
 172             }
 173
 174
 175             /* Search through conjunction which must be satisfied, and attempt
 176                to generate appropriate repair actions.
 177              */
 178             HashSet newset=new HashSet();
 179             for(Iterator cit=cantremove.iterator();cit.hasNext();) {
 180                 GraphNode gn=(GraphNode)cit.next();
 181                 boolean nomodify=true;
 182                 HashSet toremove=new HashSet();
 183                 if (termination.conjunctions.contains(gn)) {
 184                     for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 185                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 186                         GraphNode gn2=e.getTarget();
 187                         TermNode tn2=(TermNode)gn2.getOwner();
 188                         if (nodes.contains(gn2)&&
 189                             tn2.getType()==TermNode.ABSTRACT) {
 190
 191                             HashSet updateset=new HashSet();
 192                             for(Iterator upit=gn2.edges();upit.hasNext();) {
 193                                 GraphNode.Edge e2=(GraphNode.Edge)upit.next();
 194                                 GraphNode gn3=e2.getTarget();
 195                                 TermNode tn3=(TermNode)gn3.getOwner();
 196                                 if (tn3.getType()==TermNode.UPDATE)
 197                                     updateset.add(gn3);
 198                             }
 199                             updateset.removeAll(mustremove);
 200                             if (updateset.size()==1)
 201                                 toremove.addAll(updateset);
 202                         }
 203                     }
 204                     newset.addAll(toremove);
 205                 }
 206             }
 207
 208             {
 209                 int oldsize=cantremove.size();
 210                 cantremove.addAll(newset);
 211                 if (cantremove.size()!=oldsize)
 212                     change=true;
 213             }
 214
 215             /* Look for required actions for scope nodes */
 216             for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
 217                 GraphNode gn=(GraphNode)scopeit.next();
 218                 HashSet tmpset=new HashSet();
 219                 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 220                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 221                     tmpset.add(e.getTarget());
 222                 }
 223                 tmpset.removeAll(mustremove);
 224                 if (tmpset.size()==1) {
 225                     int oldsize=cantremove.size();
 226                     cantremove.addAll(tmpset);
 227                     if (cantremove.size()!=oldsize)
 228                         change=true;
 229                 }
 230             }
 231
 232             if (Compiler.AGGRESSIVESEARCH) {
 233                 /* Aggressively remove compensation nodes */
 234                 for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
 235                     GraphNode gn=(GraphNode)scopeit.next();
 236                     HashSet tmpset=new HashSet();
 237                     boolean doremove=false;
 238                     for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 239                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 240                         GraphNode gn2=e.getTarget();
 241                         if (termination.consequencenodes.contains(gn2)) {
 242                             if (((!couldremove.contains(gn2))||cantremove.contains(gn2))&&
 243                                 !mustremove.contains(gn2)) {
 244                                 doremove=true;
 245                             } else
 246                                 break;
 247                         } else tmpset.add(gn2);
 248                     }
 249                     if (doremove)
 250                         mustremove.addAll(tmpset);
 251                 }
 252             }
 253
 254             Set cycles2=GraphNode.findcycles(cantremove);
 255             for(Iterator it=cycles2.iterator();it.hasNext();) {
 256                 GraphNode gn=(GraphNode)it.next();
 257                 if (termination.conjunctions.contains(gn)) {
 258                     try {
 259                         GraphNode.DOTVisitor.visit(new FileOutputStream("graphdebug.dot"),cantremove);
 260                     } catch (Exception e) {
 261                         e.printStackTrace();
 262                         System.exit(-1);
 263                     }
 264
 265                     System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
 266                     System.out.println("CANTREMOVE");
 267                     for(Iterator it2=cantremove.iterator();it2.hasNext();) {
 268                         GraphNode gn2=(GraphNode)it2.next();
 269                         System.out.println(gn2.getTextLabel());
 270                     }
 271                     System.out.println("MUSTREMOVE");
 272                     for(Iterator it2=mustremove.iterator();it2.hasNext();) {
 273                         GraphNode gn2=(GraphNode)it2.next();
 274                         System.out.println(gn2.getTextLabel());
 275                     }
 276                     return null; // Out of luck
 277                 }
 278             }
 279
 280             /* Search through abstract repair actions & correspond data structure updates */
 281             for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
 282                 GraphNode gn=(GraphNode)it.next();
 283                 TermNode tn=(TermNode)gn.getOwner();
 284
 285                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 286                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 287                     GraphNode gn2=e.getTarget();
 288                     TermNode tn2=(TermNode)gn2.getOwner();
 289                     if (tn2.getType()!=TermNode.UPDATE)
 290                         continue;
 291
 292                     boolean containsgn=cantremove.contains(gn);
 293                     boolean containsgn2=cantremove.contains(gn2);
 294
 295                     cantremove.add(gn);
 296                     cantremove.add(gn2);
 297
 298                     Set cycle=GraphNode.findcycles(cantremove);
 299                     if (cycle.contains(gn2)) {
 300                         if (!mustremove.contains(gn2)) {
 301                             change=true;
 302                             mustremove.add(gn2);
 303                         }
 304                     }
 305                     if (!containsgn)
 306                         cantremove.remove(gn);
 307                     if (!containsgn2)
 308                         cantremove.remove(gn2);
 309                 }
 310             }
 311
 312             /* Searches individual conjunctions + abstract action +updates for cycles */
 313             for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 314                 GraphNode gn=(GraphNode)it.next();
 315                 boolean foundnocycle=false;
 316
 317                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 318                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 319                     GraphNode gn2=e.getTarget();
 320                     TermNode tn2=(TermNode)gn2.getOwner();
 321                     if (tn2.getType()!=TermNode.ABSTRACT)
 322                         continue;
 323                     AbstractRepair ar=tn2.getAbstract();
 324                     boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
 325                     int numadd=0;int numremove=0;
 326
 327                     for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 328                         GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 329                         GraphNode gn3=e2.getTarget();
 330                         TermNode tn3=(TermNode)gn3.getOwner();
 331                         if (tn3.getType()!=TermNode.UPDATE)
 332                             continue;
 333
 334                         boolean containsgn=cantremove.contains(gn);
 335                         boolean containsgn2=cantremove.contains(gn2);
 336                         boolean containsgn3=cantremove.contains(gn3);
 337                         cantremove.add(gn);
 338                         cantremove.add(gn2);
 339                         cantremove.add(gn3);
 340                         Set cycle=GraphNode.findcycles(cantremove);
 341                         if (cycle.contains(gn3)) {
 342                             if (!mustremove.contains(gn3)) {
 343                                 change=true;
 344                                 mustremove.add(gn3);
 345                             }
 346                         }
 347                         if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
 348                             foundnocycle=true;
 349                             if (ismodify) {
 350                                 MultUpdateNode mun=tn3.getUpdate();
 351                                 if (mun.getType()==MultUpdateNode.ADD)
 352                                     numadd++;
 353                                 if (mun.getType()==MultUpdateNode.REMOVE)
 354                                     numremove++;
 355                             }
 356                         }
 357                         if (!containsgn)
 358                             cantremove.remove(gn);
 359                         if (!containsgn2)
 360                             cantremove.remove(gn2);
 361                         if (!containsgn3)
 362                             cantremove.remove(gn3);
 363                     }
 364                     if (ismodify&&((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state)))) {
 365                         for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 366                             GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 367                             GraphNode gn3=e2.getTarget();
 368                             TermNode tn3=(TermNode)gn3.getOwner();
 369                             if (tn3.getType()!=TermNode.UPDATE)
 370                                 continue;
 371                             MultUpdateNode mun=tn3.getUpdate();
 372                             if (((mun.getType()==MultUpdateNode.ADD)||
 373                                 (mun.getType()==MultUpdateNode.REMOVE))&&
 374                                 (!mustremove.contains(gn3)))
 375                                 mustremove.add(gn3);
 376                         }
 377                     }
 378                 }
 379
 380                 if(!foundnocycle) {
 381                     if (!mustremove.contains(gn)) {
 382                         change=true;
 383                         mustremove.add(gn);
 384                     }
 385                 }
 386             }
 387
 388             /* Searches scope nodes + compensation nodes */
 389             for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
 390                 GraphNode gn=(GraphNode)it.next();
 391                 int count=0;
 392                 if (nodes.contains(gn)) {
 393                     for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 394                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 395                         GraphNode gn2=e.getTarget();
 396                         TermNode tn2=(TermNode)gn2.getOwner();
 397
 398                         if ((tn2.getType()==TermNode.CONSEQUENCE)&&
 399                             !mustremove.contains(gn2))
 400                             count++;
 401
 402
 403                         if (tn2.getType()!=TermNode.UPDATE)
 404                             continue;
 405                         /* We have a compensation node */
 406                         boolean containsgn=cantremove.contains(gn);
 407                         boolean containsgn2=cantremove.contains(gn2);
 408                         cantremove.add(gn);
 409                         cantremove.add(gn2);
 410
 411                         Set cycle=GraphNode.findcycles(cantremove);
 412                         if (cycle.contains(gn2)) {
 413                             if (!mustremove.contains(gn2)) {
 414                                 change=true;
 415                                 mustremove.add(gn2);
 416                             }
 417                         } else {
 418                             if (!mustremove.contains(gn2))
 419                                 count++;
 420                         }
 421                         if (!containsgn)
 422                             cantremove.remove(gn);
 423                         if (!containsgn2)
 424                             cantremove.remove(gn2);
 425                     }
 426
 427                     if (count==1) {
 428                         for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 429                             GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 430                             GraphNode gn2=e.getTarget();
 431                             TermNode tn2=(TermNode)gn2.getOwner();
 432                             if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
 433                                 !mustremove.contains(gn2)) {
 434                                 if (!cantremove.contains(gn2)) {
 435                                     cantremove.add(gn2);
 436                                     change=true;
 437                                 }
 438                             }
 439                         }
 440                     }
 441                 }
 442             }
 443             couldremove.removeAll(mustremove);
 444             couldremove.removeAll(cantremove);
 445
 446             Vector couldremovevector=new Vector();
 447             couldremovevector.addAll(couldremove);
 448             Vector combination=new Vector();
 449             if(change)
 450                 continue; //recalculate
 451
 452             try {
 453                 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
 454             } catch (Exception e) {
 455                 e.printStackTrace();
 456                 System.exit(-1);
 457             }
 458
 459             try {
 460                 GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
 461             } catch (Exception e) {
 462                 e.printStackTrace();
 463                 System.exit(-1);
 464             }
 465
 466             System.out.println("Searching set of "+couldremove.size()+" nodes.");
 467             System.out.println("Eliminated must "+mustremove.size()+" nodes");
 468             System.out.println("Eliminated cant "+cantremove.size()+" nodes");
 469             System.out.println("Searching following set:");
 470             for(Iterator it=couldremove.iterator();it.hasNext();) {
 471                 GraphNode gn=(GraphNode)it.next();
 472                 System.out.println(gn.getTextLabel());
 473             }
 474             System.out.println("Must remove set:");
 475             for(Iterator it=mustremove.iterator();it.hasNext();) {
 476                 GraphNode gn=(GraphNode)it.next();
 477                 System.out.println(gn.getTextLabel());
 478             }
 479             System.out.println("Cant remove set:");
 480             for(Iterator it=cantremove.iterator();it.hasNext();) {
 481                 GraphNode gn=(GraphNode)it.next();
 482                 System.out.println(gn.getTextLabel());
 483             }
 484
 485             System.out.println("==================================================");
 486             while(true) {
 487                 if (illegal(combination,couldremovevector))
 488                     break;
 489                 Set combinationset=buildset(combination,couldremovevector);
 490                 System.out.println("---------------------------");
 491                 for(Iterator it=combinationset.iterator();it.hasNext();) {
 492                     System.out.println(((GraphNode)it.next()).getTextLabel());
 493                 }
 494                 System.out.println("---------------------------");
 495                 checkmodify(combinationset);
 496                 combinationset.addAll(mustremove);
 497                 if (combinationset!=null) {
 498                     int checkabstract=checkAbstract(combinationset);
 499                     int checkrep=checkRepairs(combinationset);
 500                     int checkall=checkAll(combinationset);
 501
 502                     System.out.println("Checkabstract="+checkabstract);
 503                     System.out.println("Checkrepairs="+checkrep);
 504                     System.out.println("Checkall="+checkall);
 505
 506                     if (checkabstract==0&&
 507                         checkrep==0&&
 508                         checkall==0) {
 509                         return combinationset;
 510                     }
 511                 }
 512                 increment(combination,couldremovevector);
 513             }
 514             System.out.println("Search failed!");
 515             return null;
 516         }
 517     }
 518
 519     private void checkmodify(Set removednodes) {
 520         for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
 521             GraphNode gn=(GraphNode)it.next();
 522             TermNode tn=(TermNode)gn.getOwner();
 523             AbstractRepair ar=tn.getAbstract();
 524
 525             /* Has MODIFYRELATION */
 526             if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 527                 int numadd=0;
 528                 int numremove=0;
 529                 for(Iterator it2=gn.edges();it2.hasNext();) {
 530                     GraphNode.Edge edge=(GraphNode.Edge)it2.next();
 531                     GraphNode gn2=edge.getTarget();
 532                     TermNode tn2=(TermNode)gn2.getOwner();
 533                     if (!removednodes.contains(gn2)&&
 534                         tn2.getType()==TermNode.UPDATE) {
 535                         MultUpdateNode mun=tn2.getUpdate();
 536
 537                         if (mun.getType()==MultUpdateNode.ADD)
 538                             numadd++;
 539                         if (mun.getType()==MultUpdateNode.REMOVE)
 540                             numremove++;
 541                     }
 542                 }
 543                 if ((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state))) {
 544                     for(Iterator it2=gn.edges();it2.hasNext();) {
 545                         GraphNode.Edge edge=(GraphNode.Edge)it2.next();
 546                         GraphNode gn2=edge.getTarget();
 547                         TermNode tn2=(TermNode)gn2.getOwner();
 548                         if (!removednodes.contains(gn2)&&
 549                             tn2.getType()==TermNode.UPDATE) {
 550                             MultUpdateNode mun=tn2.getUpdate();
 551                             if ((mun.getType()==MultUpdateNode.ADD)
 552                                 ||(mun.getType()==MultUpdateNode.REMOVE)) {
 553                                 removednodes.add(gn2);
 554                             }
 555                         }
 556                     }
 557                 }
 558             }
 559         }
 560     }
 561
 562     private static Set buildset(Vector combination, Vector couldremove) {
 563         Set s=new HashSet();
 564         for(int i=0;i<combination.size();i++) {
 565             int index=((Integer)combination.get(i)).intValue();
 566             Object o=couldremove.get(index);
 567             if (s.contains(o))
 568                 return null;
 569             else
 570                 s.add(o);
 571         }
 572         return s;
 573     }
 574
 575     private static boolean illegal(Vector combination, Vector couldremove) {
 576         if (combination.size()>couldremove.size())
 577             return true;
 578         else return false;
 579     }
 580     private static void increment(Vector combination, Vector couldremove) {
 581         boolean incremented=false;
 582         boolean forcereset=false;
 583         for(int i=0;i<combination.size();i++) {
 584             int newindex=((Integer)combination.get(i)).intValue()+1;
 585             if (newindex==couldremove.size()||forcereset) {
 586                 forcereset=false;
 587                 if ((i+1)==combination.size()) {
 588                     newindex=1;
 589                 } else
 590                     newindex=((Integer)combination.get(i+1)).intValue()+2;
 591                 for(int j=i;j>=0;j--) {
 592                     combination.set(j,new Integer(newindex));
 593                     newindex++;
 594                 }
 595                 if (newindex>couldremove.size())
 596                     forcereset=true;
 597             } else {
 598                 incremented=true;
 599                 combination.set(i,new Integer(newindex));
 600                 break;
 601             }
 602         }
 603         if (incremented==false) /* Increase length */ {
 604             combination.add(new Integer(0));
 605             System.out.println("Expanding to: "+combination.size());
 606         }
 607     }
 608
 609     /* This function checks the graph as a whole for bad cycles */
 610     public int checkAll(Collection removed) {
 611         Set nodes=new HashSet();
 612         nodes.addAll(termination.conjunctions);
 613         nodes.removeAll(removed);
 614         GraphNode.computeclosure(nodes,removed);
 615         Set cycles=GraphNode.findcycles(nodes);
 616         for(Iterator it=cycles.iterator();it.hasNext();) {
 617             GraphNode gn=(GraphNode)it.next();
 618             TermNode tn=(TermNode)gn.getOwner();
 619             switch(tn.getType()) {
 620             case TermNode.UPDATE:
 621             case TermNode.CONJUNCTION:
 622                 return ERR_CYCLE;
 623             case TermNode.ABSTRACT:
 624             case TermNode.RULESCOPE:
 625             case TermNode.CONSEQUENCE:
 626             default:
 627                 break;
 628             }
 629         }
 630         return WORKS;
 631     }
 632
 633     /* This function checks that
 634        1) All abstract repairs have a corresponding data structure update
 635           that isn't removed.
 636        2) All scope nodes have either a consequence node or a compensation
 637           node that isn't removed.
 638      */
 639     public int checkRepairs(Collection removed) {
 640         Set nodes=new HashSet();
 641         nodes.addAll(termination.conjunctions);
 642         nodes.removeAll(removed);
 643         GraphNode.computeclosure(nodes,removed);
 644         Set toretain=new HashSet();
 645         toretain.addAll(termination.abstractrepair);
 646         toretain.addAll(termination.scopenodes);
 647         nodes.retainAll(toretain);
 648         /* Nodes is now the reachable set of abstractrepairs */
 649         /* Check to see that each has an implementation */
 650         for(Iterator it=nodes.iterator();it.hasNext();) {
 651             GraphNode gn=(GraphNode)it.next();
 652             TermNode tn=(TermNode)gn.getOwner();
 653             if (tn.getType()==TermNode.RULESCOPE) {
 654                 boolean foundnode=false;
 655                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 656                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 657                     GraphNode gn2=edge.getTarget();
 658                     if (!removed.contains(gn2)) {
 659                         TermNode tn2=(TermNode)gn2.getOwner();
 660                         if ((tn2.getType()==TermNode.CONSEQUENCE)||
 661                             (tn2.getType()==TermNode.UPDATE)) {
 662                             foundnode=true;
 663                             break;
 664                         }
 665                     }
 666                 }
 667                 if (!foundnode) {
 668                     System.out.println(gn.getTextLabel());
 669                     return ERR_RULE;
 670                 }
 671             } else if (tn.getType()==TermNode.ABSTRACT) {
 672                 boolean foundnode=false;
 673                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 674                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 675                     GraphNode gn2=edge.getTarget();
 676                     if (!removed.contains(gn2)) {
 677                         TermNode tn2=(TermNode)gn2.getOwner();
 678                         if (tn2.getType()==TermNode.UPDATE) {
 679                             foundnode=true;
 680                             break;
 681                         }
 682                     }
 683                 }
 684                 if (!foundnode)
 685                     return ERR_ABSTRACT;
 686             } else throw new Error("Unanticipated Node");
 687         }
 688         return WORKS;
 689     }
 690     /* This method checks that all constraints have conjunction nodes
 691        and that there are no bad cycles in the abstract portion of the graph.
 692      */
 693     public int checkAbstract(Collection removed) {
 694         Vector constraints=termination.state.vConstraints;
 695         for(int i=0;i<constraints.size();i++) {
 696             Constraint c=(Constraint)constraints.get(i);
 697             Set conjunctionset=(Set)termination.conjunctionmap.get(c);
 698
 699             boolean foundrepair=false;
 700             for(Iterator it=conjunctionset.iterator();it.hasNext();) {
 701                 GraphNode gn=(GraphNode)it.next();
 702                 if (!removed.contains(gn)) {
 703                     foundrepair=true;
 704                 }
 705             }
 706             if (!foundrepair)
 707                 return ERR_NOREPAIR;
 708         }
 709
 710
 711         Set abstractnodes=new HashSet();
 712         abstractnodes.addAll(termination.conjunctions);
 713         abstractnodes.removeAll(removed);
 714         GraphNode.computeclosure(abstractnodes,removed);
 715
 716         Set tset=new HashSet();
 717         tset.addAll(termination.conjunctions);
 718         tset.addAll(termination.abstractrepair);
 719         tset.addAll(termination.scopenodes);
 720         tset.addAll(termination.consequencenodes);
 721         abstractnodes.retainAll(tset);
 722         Set cycles=GraphNode.findcycles(abstractnodes);
 723
 724         for(Iterator it=cycles.iterator();it.hasNext();) {
 725             GraphNode gn=(GraphNode)it.next();
 726             System.out.println("NODE: "+gn.getTextLabel());
 727             TermNode tn=(TermNode)gn.getOwner();
 728             switch(tn.getType()) {
 729             case TermNode.CONJUNCTION:
 730             case TermNode.ABSTRACT:
 731                 return ERR_CYCLE;
 732             case TermNode.UPDATE:
 733                 throw new Error("No Update Nodes should be here");
 734             default:
 735             }
 736         }
 737         return WORKS;
 738     }
 739 }