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                 boolean foundnocycle=false;
 358
 359                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 360                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 361                     GraphNode gn2=e.getTarget();
 362                     TermNode tn2=(TermNode)gn2.getOwner();
 363                     if (tn2.getType()!=TermNode.ABSTRACT)
 364                         continue;
 365                     AbstractRepair ar=tn2.getAbstract();
 366                     boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
 367                     int numadd=0;int numremove=0;
 368
 369                     for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 370                         GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 371                         GraphNode gn3=e2.getTarget();
 372                         TermNode tn3=(TermNode)gn3.getOwner();
 373                         if (tn3.getType()!=TermNode.UPDATE)
 374                             continue;
 375
 376                         boolean containsgn=cantremove.contains(gn);
 377                         boolean containsgn2=cantremove.contains(gn2);
 378                         boolean containsgn3=cantremove.contains(gn3);
 379                         cantremove.add(gn);
 380                         cantremove.add(gn2);
 381                         cantremove.add(gn3);
 382                         Set cycle=GraphNode.findcycles(cantremove);
 383                         if (cycle.contains(gn3)) {
 384                             if (!mustremove.contains(gn3)) {
 385                                 change=true;
 386                                 mustremove.add(gn3);
 387                             }
 388                         }
 389                         if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
 390                             foundnocycle=true;
 391                             if (ismodify) {
 392                                 MultUpdateNode mun=tn3.getUpdate();
 393                                 if (mun.getType()==MultUpdateNode.ADD)
 394                                     numadd++;
 395                                 if (mun.getType()==MultUpdateNode.REMOVE)
 396                                     numremove++;
 397                             }
 398                         }
 399                         if (!containsgn)
 400                             cantremove.remove(gn);
 401                         if (!containsgn2)
 402                             cantremove.remove(gn2);
 403                         if (!containsgn3)
 404                             cantremove.remove(gn3);
 405                     }
 406                     if (ismodify&&((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state)))) {
 407                         for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 408                             GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 409                             GraphNode gn3=e2.getTarget();
 410                             TermNode tn3=(TermNode)gn3.getOwner();
 411                             if (tn3.getType()!=TermNode.UPDATE)
 412                                 continue;
 413                             MultUpdateNode mun=tn3.getUpdate();
 414                             if (((mun.getType()==MultUpdateNode.ADD)||
 415                                 (mun.getType()==MultUpdateNode.REMOVE))&&
 416                                 (!mustremove.contains(gn3)))
 417                                 mustremove.add(gn3);
 418                         }
 419                     }
 420                 }
 421
 422                 if(!foundnocycle) {
 423                     if (!mustremove.contains(gn)) {
 424                         change=true;
 425                         mustremove.add(gn);
 426                     }
 427                 }
 428             }
 429
 430             /* Searches scope nodes + compensation nodes */
 431             for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
 432                 GraphNode gn=(GraphNode)it.next();
 433                 if (nodes.contains(gn)) {
 434                     for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 435                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 436                         GraphNode gn2=e.getTarget();
 437                         TermNode tn2=(TermNode)gn2.getOwner();
 438
 439                         if (tn2.getType()!=TermNode.UPDATE)
 440                             continue;
 441                         /* We have a compensation node */
 442                         boolean containsgn=cantremove.contains(gn);
 443                         boolean containsgn2=cantremove.contains(gn2);
 444                         cantremove.add(gn);
 445                         cantremove.add(gn2);
 446
 447                         Set cycle=GraphNode.findcycles(cantremove);
 448                         if (cycle.contains(gn2)) {
 449                             if (!mustremove.contains(gn2)) {
 450                                 change=true;
 451                                 mustremove.add(gn2);
 452                             }
 453                         }
 454                         if (!containsgn)
 455                             cantremove.remove(gn);
 456                         if (!containsgn2)
 457                             cantremove.remove(gn2);
 458                     }
 459                 }
 460             }
 461             couldremove.removeAll(mustremove);
 462             couldremove.removeAll(cantremove);
 463
 464             Vector couldremovevector=new Vector();
 465             couldremovevector.addAll(couldremove);
 466             Vector combination=new Vector();
 467             if(change)
 468                 continue; //recalculate
 469
 470             try {
 471                 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
 472             } catch (Exception e) {
 473                 e.printStackTrace();
 474                 System.exit(-1);
 475             }
 476
 477             try {
 478                 GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
 479             } catch (Exception e) {
 480                 e.printStackTrace();
 481                 System.exit(-1);
 482             }
 483
 484             System.out.println("Searching set of "+couldremove.size()+" nodes.");
 485             System.out.println("Eliminated must "+mustremove.size()+" nodes");
 486             System.out.println("Eliminated cant "+cantremove.size()+" nodes");
 487             System.out.println("Searching following set:");
 488             for(Iterator it=couldremove.iterator();it.hasNext();) {
 489                 GraphNode gn=(GraphNode)it.next();
 490                 System.out.println(gn.getTextLabel());
 491             }
 492             System.out.println("Must remove set:");
 493             for(Iterator it=mustremove.iterator();it.hasNext();) {
 494                 GraphNode gn=(GraphNode)it.next();
 495                 System.out.println(gn.getTextLabel());
 496             }
 497             System.out.println("Cant remove set:");
 498             for(Iterator it=cantremove.iterator();it.hasNext();) {
 499                 GraphNode gn=(GraphNode)it.next();
 500                 System.out.println(gn.getTextLabel());
 501             }
 502
 503             System.out.println("==================================================");
 504             while(true) {
 505                 if (illegal(combination,couldremovevector))
 506                     break;
 507                 Set combinationset=buildset(combination,couldremovevector);
 508                 System.out.println("---------------------------");
 509                 for(Iterator it=combinationset.iterator();it.hasNext();) {
 510                     System.out.println(((GraphNode)it.next()).getTextLabel());
 511                 }
 512                 System.out.println("---------------------------");
 513                 checkmodify(combinationset);
 514                 combinationset.addAll(mustremove);
 515                 if (combinationset!=null) {
 516                     int checkabstract=checkAbstract(combinationset);
 517                     int checkrep=checkRepairs(combinationset);
 518                     int checkall=checkAll(combinationset);
 519
 520                     System.out.println("Checkabstract="+checkabstract);
 521                     System.out.println("Checkrepairs="+checkrep);
 522                     System.out.println("Checkall="+checkall);
 523
 524                     if (checkabstract==0&&
 525                         checkrep==0&&
 526                         checkall==0) {
 527                         return combinationset;
 528                     }
 529                 }
 530                 increment(combination,couldremovevector);
 531             }
 532             System.out.println("Search failed!");
 533             return null;
 534         }
 535     }
 536
 537     private void checkmodify(Set removednodes) {
 538         for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
 539             GraphNode gn=(GraphNode)it.next();
 540             TermNode tn=(TermNode)gn.getOwner();
 541             AbstractRepair ar=tn.getAbstract();
 542
 543             /* Has MODIFYRELATION */
 544             if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 545                 int numadd=0;
 546                 int numremove=0;
 547                 for(Iterator it2=gn.edges();it2.hasNext();) {
 548                     GraphNode.Edge edge=(GraphNode.Edge)it2.next();
 549                     GraphNode gn2=edge.getTarget();
 550                     TermNode tn2=(TermNode)gn2.getOwner();
 551                     if (!removednodes.contains(gn2)&&
 552                         tn2.getType()==TermNode.UPDATE) {
 553                         MultUpdateNode mun=tn2.getUpdate();
 554
 555                         if (mun.getType()==MultUpdateNode.ADD)
 556                             numadd++;
 557                         if (mun.getType()==MultUpdateNode.REMOVE)
 558                             numremove++;
 559                     }
 560                 }
 561                 if ((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state))) {
 562                     for(Iterator it2=gn.edges();it2.hasNext();) {
 563                         GraphNode.Edge edge=(GraphNode.Edge)it2.next();
 564                         GraphNode gn2=edge.getTarget();
 565                         TermNode tn2=(TermNode)gn2.getOwner();
 566                         if (!removednodes.contains(gn2)&&
 567                             tn2.getType()==TermNode.UPDATE) {
 568                             MultUpdateNode mun=tn2.getUpdate();
 569                             if ((mun.getType()==MultUpdateNode.ADD)
 570                                 ||(mun.getType()==MultUpdateNode.REMOVE)) {
 571                                 removednodes.add(gn2);
 572                             }
 573                         }
 574                     }
 575                 }
 576             }
 577         }
 578     }
 579
 580     private static Set buildset(Vector combination, Vector couldremove) {
 581         Set s=new HashSet();
 582         for(int i=0;i<combination.size();i++) {
 583             int index=((Integer)combination.get(i)).intValue();
 584             Object o=couldremove.get(index);
 585             if (s.contains(o))
 586                 return null;
 587             else
 588                 s.add(o);
 589         }
 590         return s;
 591     }
 592
 593     private static boolean illegal(Vector combination, Vector couldremove) {
 594         if (combination.size()>couldremove.size())
 595             return true;
 596         else return false;
 597     }
 598     private static void increment(Vector combination, Vector couldremove) {
 599         boolean incremented=false;
 600         boolean forcereset=false;
 601         for(int i=0;i<combination.size();i++) {
 602             int newindex=((Integer)combination.get(i)).intValue()+1;
 603             if (newindex==couldremove.size()||forcereset) {
 604                 forcereset=false;
 605                 if ((i+1)==combination.size()) {
 606                     newindex=1;
 607                 } else
 608                     newindex=((Integer)combination.get(i+1)).intValue()+2;
 609                 for(int j=i;j>=0;j--) {
 610                     combination.set(j,new Integer(newindex));
 611                     newindex++;
 612                 }
 613                 if (newindex>couldremove.size())
 614                     forcereset=true;
 615             } else {
 616                 incremented=true;
 617                 combination.set(i,new Integer(newindex));
 618                 break;
 619             }
 620         }
 621         if (incremented==false) /* Increase length */ {
 622             combination.add(new Integer(0));
 623             System.out.println("Expanding to: "+combination.size());
 624         }
 625     }
 626
 627     /* This function checks the graph as a whole for bad cycles */
 628     public int checkAll(Collection removed) {
 629         Set nodes=new HashSet();
 630         nodes.addAll(termination.conjunctions);
 631         nodes.removeAll(removed);
 632         GraphNode.computeclosure(nodes,removed);
 633         Set cycles=GraphNode.findcycles(nodes);
 634         for(Iterator it=cycles.iterator();it.hasNext();) {
 635             GraphNode gn=(GraphNode)it.next();
 636             TermNode tn=(TermNode)gn.getOwner();
 637             switch(tn.getType()) {
 638             case TermNode.UPDATE:
 639             case TermNode.CONJUNCTION:
 640                 return ERR_CYCLE;
 641             case TermNode.ABSTRACT:
 642             case TermNode.RULESCOPE:
 643             case TermNode.CONSEQUENCE:
 644             default:
 645                 break;
 646             }
 647         }
 648         return WORKS;
 649     }
 650
 651     /* This function checks that
 652        1) All abstract repairs have a corresponding data structure update
 653           that isn't removed.
 654        2) All scope nodes have either a consequence node or a compensation
 655           node that isn't removed.
 656      */
 657     public int checkRepairs(Collection removed) {
 658         Set nodes=new HashSet();
 659         nodes.addAll(termination.conjunctions);
 660         nodes.removeAll(removed);
 661         GraphNode.computeclosure(nodes,removed);
 662         Set toretain=new HashSet();
 663         toretain.addAll(termination.abstractrepair);
 664         toretain.addAll(termination.scopenodes);
 665         nodes.retainAll(toretain);
 666         /* Nodes is now the reachable set of abstractrepairs */
 667         /* Check to see that each has an implementation */
 668         for(Iterator it=nodes.iterator();it.hasNext();) {
 669             GraphNode gn=(GraphNode)it.next();
 670             TermNode tn=(TermNode)gn.getOwner();
 671             if (tn.getType()==TermNode.RULESCOPE) {
 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.CONSEQUENCE)||
 679                             (tn2.getType()==TermNode.UPDATE)) {
 680                             foundnode=true;
 681                             break;
 682                         }
 683                     }
 684                 }
 685                 if (!foundnode) {
 686                     System.out.println(gn.getTextLabel());
 687                     return ERR_RULE;
 688                 }
 689             } else if (tn.getType()==TermNode.ABSTRACT) {
 690                 boolean foundnode=false;
 691                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 692                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 693                     GraphNode gn2=edge.getTarget();
 694                     if (!removed.contains(gn2)) {
 695                         TermNode tn2=(TermNode)gn2.getOwner();
 696                         if (tn2.getType()==TermNode.UPDATE) {
 697                             foundnode=true;
 698                             break;
 699                         }
 700                     }
 701                 }
 702                 if (!foundnode)
 703                     return ERR_ABSTRACT;
 704             } else throw new Error("Unanticipated Node");
 705         }
 706         return WORKS;
 707     }
 708     /* This method checks that all constraints have conjunction nodes
 709        and that there are no bad cycles in the abstract portion of the graph.
 710      */
 711     public int checkAbstract(Collection removed) {
 712         Vector constraints=termination.state.vConstraints;
 713         for(int i=0;i<constraints.size();i++) {
 714             Constraint c=(Constraint)constraints.get(i);
 715             Set conjunctionset=(Set)termination.conjunctionmap.get(c);
 716
 717             boolean foundrepair=false;
 718             for(Iterator it=conjunctionset.iterator();it.hasNext();) {
 719                 GraphNode gn=(GraphNode)it.next();
 720                 if (!removed.contains(gn)) {
 721                     foundrepair=true;
 722                 }
 723             }
 724             if (!foundrepair)
 725                 return ERR_NOREPAIR;
 726         }
 727
 728
 729         Set abstractnodes=new HashSet();
 730         abstractnodes.addAll(termination.conjunctions);
 731         abstractnodes.removeAll(removed);
 732         GraphNode.computeclosure(abstractnodes,removed);
 733
 734         Set tset=new HashSet();
 735         tset.addAll(termination.conjunctions);
 736         tset.addAll(termination.abstractrepair);
 737         tset.addAll(termination.scopenodes);
 738         tset.addAll(termination.consequencenodes);
 739         abstractnodes.retainAll(tset);
 740         Set cycles=GraphNode.findcycles(abstractnodes);
 741
 742         for(Iterator it=cycles.iterator();it.hasNext();) {
 743             GraphNode gn=(GraphNode)it.next();
 744             System.out.println("NODE: "+gn.getTextLabel());
 745             TermNode tn=(TermNode)gn.getOwner();
 746             switch(tn.getType()) {
 747             case TermNode.CONJUNCTION:
 748             case TermNode.ABSTRACT:
 749                 return ERR_CYCLE;
 750             case TermNode.UPDATE:
 751                 throw new Error("No Update Nodes should be here");
 752             default:
 753             }
 754         }
 755         return WORKS;
 756     }
 757 }