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