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