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                     System.out.println("CANTREMOVE");
 265                     for(Iterator it2=cantremove.iterator();it2.hasNext();) {
 266                         GraphNode gn2=(GraphNode)it2.next();
 267                         System.out.println(gn2.getTextLabel());
 268                     }
 269                     System.out.println("MUSTREMOVE");
 270                     for(Iterator it2=mustremove.iterator();it2.hasNext();) {
 271                         GraphNode gn2=(GraphNode)it2.next();
 272                         System.out.println(gn2.getTextLabel());
 273                     }
 274                     return null; // Out of luck
 275                 }
 276             }
 277
 278             /* Search through abstract repair actions & correspond data structure updates */
 279             for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
 280                 GraphNode gn=(GraphNode)it.next();
 281                 TermNode tn=(TermNode)gn.getOwner();
 282
 283                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 284                     GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 285                     GraphNode gn2=e.getTarget();
 286                     TermNode tn2=(TermNode)gn2.getOwner();
 287                     if (tn2.getType()!=TermNode.UPDATE)
 288                         continue;
 289
 290                     boolean containsgn=cantremove.contains(gn);
 291                     boolean containsgn2=cantremove.contains(gn2);
 292
 293                     cantremove.add(gn);
 294                     cantremove.add(gn2);
 295
 296                     Set cycle=GraphNode.findcycles(cantremove);
 297                     if (cycle.contains(gn2)) {
 298                         if (!mustremove.contains(gn2)) {
 299                             change=true;
 300                             mustremove.add(gn2);
 301                         }
 302                     }
 303                     if (!containsgn)
 304                         cantremove.remove(gn);
 305                     if (!containsgn2)
 306                         cantremove.remove(gn2);
 307                 }
 308             }
 309
 310             /* Searches individual conjunctions + abstract action +updates for cycles */
 311             for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
 312                 GraphNode gn=(GraphNode)it.next();
 313                 boolean foundnocycle=false;
 314
 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                     if (tn2.getType()!=TermNode.ABSTRACT)
 320                         continue;
 321                     AbstractRepair ar=tn2.getAbstract();
 322                     boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
 323                     int numadd=0;int numremove=0;
 324
 325                     for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 326                         GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 327                         GraphNode gn3=e2.getTarget();
 328                         TermNode tn3=(TermNode)gn3.getOwner();
 329                         if (tn3.getType()!=TermNode.UPDATE)
 330                             continue;
 331
 332                         boolean containsgn=cantremove.contains(gn);
 333                         boolean containsgn2=cantremove.contains(gn2);
 334                         boolean containsgn3=cantremove.contains(gn3);
 335                         cantremove.add(gn);
 336                         cantremove.add(gn2);
 337                         cantremove.add(gn3);
 338                         Set cycle=GraphNode.findcycles(cantremove);
 339                         if (cycle.contains(gn3)) {
 340                             if (!mustremove.contains(gn3)) {
 341                                 change=true;
 342                                 mustremove.add(gn3);
 343                             }
 344                         }
 345                         if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
 346                             foundnocycle=true;
 347                             if (ismodify) {
 348                                 MultUpdateNode mun=tn3.getUpdate();
 349                                 if (mun.getType()==MultUpdateNode.ADD)
 350                                     numadd++;
 351                                 if (mun.getType()==MultUpdateNode.REMOVE)
 352                                     numremove++;
 353                             }
 354                         }
 355                         if (!containsgn)
 356                             cantremove.remove(gn);
 357                         if (!containsgn2)
 358                             cantremove.remove(gn2);
 359                         if (!containsgn3)
 360                             cantremove.remove(gn3);
 361                     }
 362                     if (ismodify&&((numadd==0)||(numremove==0))) {
 363                         for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 364                             GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
 365                             GraphNode gn3=e2.getTarget();
 366                             TermNode tn3=(TermNode)gn3.getOwner();
 367                             if (tn3.getType()!=TermNode.UPDATE)
 368                                 continue;
 369                             MultUpdateNode mun=tn3.getUpdate();
 370                             if (((mun.getType()==MultUpdateNode.ADD)||
 371                                 (mun.getType()==MultUpdateNode.REMOVE))&&
 372                                 (!mustremove.contains(gn3)))
 373                                 mustremove.add(gn3);
 374                         }
 375                     }
 376                 }
 377
 378                 if(!foundnocycle) {
 379                     if (!mustremove.contains(gn)) {
 380                         change=true;
 381                         mustremove.add(gn);
 382                     }
 383                 }
 384             }
 385
 386             /* Searches scope nodes + compensation nodes */
 387             for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
 388                 GraphNode gn=(GraphNode)it.next();
 389                 int count=0;
 390                 if (nodes.contains(gn)) {
 391                     for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 392                         GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 393                         GraphNode gn2=e.getTarget();
 394                         TermNode tn2=(TermNode)gn2.getOwner();
 395
 396                         if ((tn2.getType()==TermNode.CONSEQUENCE)&&
 397                             !mustremove.contains(gn2))
 398                             count++;
 399
 400
 401                         if (tn2.getType()!=TermNode.UPDATE)
 402                             continue;
 403                         /* We have a compensation node */
 404                         boolean containsgn=cantremove.contains(gn);
 405                         boolean containsgn2=cantremove.contains(gn2);
 406                         cantremove.add(gn);
 407                         cantremove.add(gn2);
 408
 409                         Set cycle=GraphNode.findcycles(cantremove);
 410                         if (cycle.contains(gn2)) {
 411                             if (!mustremove.contains(gn2)) {
 412                                 change=true;
 413                                 mustremove.add(gn2);
 414                             }
 415                         } else {
 416                             if (!mustremove.contains(gn2))
 417                                 count++;
 418                         }
 419                         if (!containsgn)
 420                             cantremove.remove(gn);
 421                         if (!containsgn2)
 422                             cantremove.remove(gn2);
 423                     }
 424
 425                     if (count==1) {
 426                         for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 427                             GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
 428                             GraphNode gn2=e.getTarget();
 429                             TermNode tn2=(TermNode)gn2.getOwner();
 430                             if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
 431                                 !mustremove.contains(gn2)) {
 432                                 if (!cantremove.contains(gn2)) {
 433                                     cantremove.add(gn2);
 434                                     change=true;
 435                                 }
 436                             }
 437                         }
 438                     }
 439                 }
 440             }
 441             couldremove.removeAll(mustremove);
 442             couldremove.removeAll(cantremove);
 443
 444             Vector couldremovevector=new Vector();
 445             couldremovevector.addAll(couldremove);
 446             Vector combination=new Vector();
 447             if(change)
 448                 continue; //recalculate
 449
 450             try {
 451                 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
 452             } catch (Exception e) {
 453                 e.printStackTrace();
 454                 System.exit(-1);
 455             }
 456
 457             try {
 458                 GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
 459             } catch (Exception e) {
 460                 e.printStackTrace();
 461                 System.exit(-1);
 462             }
 463
 464             System.out.println("Searching set of "+couldremove.size()+" nodes.");
 465             System.out.println("Eliminated must "+mustremove.size()+" nodes");
 466             System.out.println("Eliminated cant "+cantremove.size()+" nodes");
 467             System.out.println("Searching following set:");
 468             for(Iterator it=couldremove.iterator();it.hasNext();) {
 469                 GraphNode gn=(GraphNode)it.next();
 470                 System.out.println(gn.getTextLabel());
 471             }
 472             System.out.println("Must remove set:");
 473             for(Iterator it=mustremove.iterator();it.hasNext();) {
 474                 GraphNode gn=(GraphNode)it.next();
 475                 System.out.println(gn.getTextLabel());
 476             }
 477             System.out.println("Cant remove set:");
 478             for(Iterator it=cantremove.iterator();it.hasNext();) {
 479                 GraphNode gn=(GraphNode)it.next();
 480                 System.out.println(gn.getTextLabel());
 481             }
 482
 483
 484             while(true) {
 485                 if (illegal(combination,couldremovevector))
 486                     break;
 487                 Set combinationset=buildset(combination,couldremovevector);
 488                 checkmodify(combinationset);
 489                 combinationset.addAll(mustremove);
 490                 if (combinationset!=null) {
 491                     System.out.println("Checkabstract="+checkAbstract(combinationset));
 492                     System.out.println("Checkrepairs="+checkRepairs(combinationset));
 493                     System.out.println("Checkall="+checkAll(combinationset));
 494
 495                     if (checkAbstract(combinationset)==0&&
 496                         checkRepairs(combinationset)==0&&
 497                         checkAll(combinationset)==0) {
 498                         return combinationset;
 499                     }
 500                 }
 501                 increment(combination,couldremovevector);
 502             }
 503             System.out.println("Search failed!");
 504             return null;
 505         }
 506     }
 507
 508     private void checkmodify(Set removednodes) {
 509         for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
 510             GraphNode gn=(GraphNode)it.next();
 511             TermNode tn=(TermNode)gn.getOwner();
 512             AbstractRepair ar=tn.getAbstract();
 513
 514             /* Has MODIFYRELATION */
 515             if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 516                 int numadd=0;
 517                 int numremove=0;
 518                 for(Iterator it2=gn.edges();it2.hasNext();) {
 519                     GraphNode.Edge edge=(GraphNode.Edge)it2.next();
 520                     GraphNode gn2=edge.getTarget();
 521                     TermNode tn2=(TermNode)gn2.getOwner();
 522                     if (!removednodes.contains(gn2)&&
 523                         tn2.getType()==TermNode.UPDATE) {
 524                         MultUpdateNode mun=tn2.getUpdate();
 525
 526                         if (mun.getType()==MultUpdateNode.ADD)
 527                             numadd++;
 528                         if (mun.getType()==MultUpdateNode.REMOVE)
 529                             numremove++;
 530                     }
 531                 }
 532                 if ((numadd==0)||(numremove==0)) {
 533                     for(Iterator it2=gn.edges();it2.hasNext();) {
 534                         GraphNode.Edge edge=(GraphNode.Edge)it2.next();
 535                         GraphNode gn2=edge.getTarget();
 536                         TermNode tn2=(TermNode)gn2.getOwner();
 537                         if (!removednodes.contains(gn2)&&
 538                             tn2.getType()==TermNode.UPDATE) {
 539                             MultUpdateNode mun=tn2.getUpdate();
 540                             if ((mun.getType()==MultUpdateNode.ADD)
 541                                 ||(mun.getType()==MultUpdateNode.REMOVE)) {
 542                                 removednodes.add(gn2);
 543                             }
 544                         }
 545                     }
 546                 }
 547             }
 548         }
 549     }
 550
 551     private static Set buildset(Vector combination, Vector couldremove) {
 552         Set s=new HashSet();
 553         for(int i=0;i<combination.size();i++) {
 554             int index=((Integer)combination.get(i)).intValue();
 555             Object o=couldremove.get(index);
 556             if (s.contains(o))
 557                 return null;
 558             else
 559                 s.add(o);
 560         }
 561         return s;
 562     }
 563
 564     private static boolean illegal(Vector combination, Vector couldremove) {
 565         if (combination.size()>couldremove.size())
 566             return true;
 567         else return false;
 568     }
 569     private static void increment(Vector combination, Vector couldremove) {
 570         boolean incremented=false;
 571         boolean forcereset=false;
 572         for(int i=0;i<combination.size();i++) {
 573             int newindex=((Integer)combination.get(i)).intValue()+1;
 574             if (newindex==couldremove.size()||forcereset) {
 575                 forcereset=false;
 576                 if ((i+1)==combination.size()) {
 577                     newindex=1;
 578                 } else
 579                     newindex=((Integer)combination.get(i+1)).intValue()+2;
 580                 for(int j=i;j>=0;j--) {
 581                     combination.set(j,new Integer(newindex));
 582                     newindex++;
 583                 }
 584                 if (newindex>couldremove.size())
 585                     forcereset=true;
 586             } else {
 587                 incremented=true;
 588                 combination.set(i,new Integer(newindex));
 589                 break;
 590             }
 591         }
 592         if (incremented==false) /* Increase length */ {
 593             combination.add(new Integer(0));
 594             System.out.println("Expanding to: "+combination.size());
 595         }
 596     }
 597
 598     /* This function checks the graph as a whole for bad cycles */
 599     public int checkAll(Collection removed) {
 600         Set nodes=new HashSet();
 601         nodes.addAll(termination.conjunctions);
 602         nodes.removeAll(removed);
 603         GraphNode.computeclosure(nodes,removed);
 604         Set cycles=GraphNode.findcycles(nodes);
 605         for(Iterator it=cycles.iterator();it.hasNext();) {
 606             GraphNode gn=(GraphNode)it.next();
 607             TermNode tn=(TermNode)gn.getOwner();
 608             switch(tn.getType()) {
 609             case TermNode.UPDATE:
 610             case TermNode.CONJUNCTION:
 611                 return ERR_CYCLE;
 612             case TermNode.ABSTRACT:
 613             case TermNode.RULESCOPE:
 614             case TermNode.CONSEQUENCE:
 615             default:
 616                 break;
 617             }
 618         }
 619         return WORKS;
 620     }
 621
 622     /* This function checks that
 623        1) All abstract repairs have a corresponding data structure update
 624           that isn't removed.
 625        2) All scope nodes have either a consequence node or a compensation
 626           node that isn't removed.
 627      */
 628     public int checkRepairs(Collection removed) {
 629         Set nodes=new HashSet();
 630         nodes.addAll(termination.conjunctions);
 631         nodes.removeAll(removed);
 632         GraphNode.computeclosure(nodes,removed);
 633         Set toretain=new HashSet();
 634         toretain.addAll(termination.abstractrepair);
 635         toretain.addAll(termination.scopenodes);
 636         nodes.retainAll(toretain);
 637         /* Nodes is now the reachable set of abstractrepairs */
 638         /* Check to see that each has an implementation */
 639         for(Iterator it=nodes.iterator();it.hasNext();) {
 640             GraphNode gn=(GraphNode)it.next();
 641             TermNode tn=(TermNode)gn.getOwner();
 642             if (tn.getType()==TermNode.RULESCOPE) {
 643                 boolean foundnode=false;
 644                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 645                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 646                     GraphNode gn2=edge.getTarget();
 647                     if (!removed.contains(gn2)) {
 648                         TermNode tn2=(TermNode)gn2.getOwner();
 649                         if ((tn2.getType()==TermNode.CONSEQUENCE)||
 650                             (tn2.getType()==TermNode.UPDATE)) {
 651                             foundnode=true;
 652                             break;
 653                         }
 654                     }
 655                 }
 656                 if (!foundnode) {
 657                     System.out.println(gn.getTextLabel());
 658                     return ERR_RULE;
 659                 }
 660             } else if (tn.getType()==TermNode.ABSTRACT) {
 661                 boolean foundnode=false;
 662                 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
 663                     GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 664                     GraphNode gn2=edge.getTarget();
 665                     if (!removed.contains(gn2)) {
 666                         TermNode tn2=(TermNode)gn2.getOwner();
 667                         if (tn2.getType()==TermNode.UPDATE) {
 668                             foundnode=true;
 669                             break;
 670                         }
 671                     }
 672                 }
 673                 if (!foundnode)
 674                     return ERR_ABSTRACT;
 675             } else throw new Error("Unanticipated Node");
 676         }
 677         return WORKS;
 678     }
 679     /* This method checks that all constraints have conjunction nodes
 680        and that there are no bad cycles in the abstract portion of the graph.
 681      */
 682     public int checkAbstract(Collection removed) {
 683         Vector constraints=termination.state.vConstraints;
 684         for(int i=0;i<constraints.size();i++) {
 685             Constraint c=(Constraint)constraints.get(i);
 686             Set conjunctionset=(Set)termination.conjunctionmap.get(c);
 687
 688             boolean foundrepair=false;
 689             for(Iterator it=conjunctionset.iterator();it.hasNext();) {
 690                 GraphNode gn=(GraphNode)it.next();
 691                 if (!removed.contains(gn)) {
 692                     foundrepair=true;
 693                 }
 694             }
 695             if (!foundrepair)
 696                 return ERR_NOREPAIR;
 697         }
 698
 699
 700         Set abstractnodes=new HashSet();
 701         abstractnodes.addAll(termination.conjunctions);
 702         abstractnodes.removeAll(removed);
 703         GraphNode.computeclosure(abstractnodes,removed);
 704
 705         Set tset=new HashSet();
 706         tset.addAll(termination.conjunctions);
 707         tset.addAll(termination.abstractrepair);
 708         tset.addAll(termination.scopenodes);
 709         tset.addAll(termination.consequencenodes);
 710         abstractnodes.retainAll(tset);
 711         Set cycles=GraphNode.findcycles(abstractnodes);
 712
 713         for(Iterator it=cycles.iterator();it.hasNext();) {
 714             GraphNode gn=(GraphNode)it.next();
 715             System.out.println("NODE: "+gn.getTextLabel());
 716             TermNode tn=(TermNode)gn.getOwner();
 717             switch(tn.getType()) {
 718             case TermNode.CONJUNCTION:
 719             case TermNode.ABSTRACT:
 720                 return ERR_CYCLE;
 721             case TermNode.UPDATE:
 722                 throw new Error("No Update Nodes should be here");
 723             default:
 724             }
 725         }
 726         return WORKS;
 727     }
 728 }