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