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