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