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