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