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