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;
15 public GraphAnalysis(Termination t) {
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();
25 while(!workset.empty()) {
26 GraphNode gn2=(GraphNode)workset.pop();
27 if (!closureset.contains(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))
34 if (((cantremove.contains(gn2)||!couldremove.contains(gn2))
35 &&termination.conjunctions.contains(gn2))||
36 cantremovetrans.contains(gn2))
37 cantremovetrans.add(gn3);
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)) {
51 if ((!couldremove.contains(gn3))||cantremove.contains(gn3))
56 if (termination.scopenodes.contains(gn2))
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))
74 public Set doAnalysis() {
75 HashSet cantremove=new HashSet();
76 HashSet mustremove=new HashSet();
78 cantremove.addAll(termination.scopenodes);
79 cantremove.addAll(termination.abstractrepair);
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);
95 /* Check for consequence nodes which are fine */
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);
104 /* Check for update nodes which are fine */
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);
113 /* Check for conjunction nodes which are fine */
115 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
116 GraphNode gn=(GraphNode) it.next();
117 if (mustremove.contains(gn)||cantremove.contains(gn))
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)
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());
155 /* Look for constraints which can only be satisfied one way */
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)
173 /* Search through conjunction which must be satisfied, and attempt
174 to generate appropriate repair actions.
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) {
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)
197 updateset.removeAll(mustremove);
198 if (updateset.size()==1)
199 toremove.addAll(updateset);
202 newset.addAll(toremove);
207 int oldsize=cantremove.size();
208 cantremove.addAll(newset);
209 if (cantremove.size()!=oldsize)
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());
221 tmpset.removeAll(mustremove);
222 if (tmpset.size()==1) {
223 int oldsize=cantremove.size();
224 cantremove.addAll(tmpset);
225 if (cantremove.size()!=oldsize)
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)) {
245 } else tmpset.add(gn2);
248 mustremove.addAll(tmpset);
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)) {
257 GraphNode.DOTVisitor.visit(new FileOutputStream("graphdebug.dot"),cantremove);
258 } catch (Exception e) {
263 System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
264 return null; // Out of luck
268 /* Search through abstract repair actions & correspond data structure updates */
269 for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
270 GraphNode gn=(GraphNode)it.next();
271 TermNode tn=(TermNode)gn.getOwner();
273 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
274 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
275 GraphNode gn2=e.getTarget();
276 TermNode tn2=(TermNode)gn2.getOwner();
277 if (tn2.getType()!=TermNode.UPDATE)
280 boolean containsgn=cantremove.contains(gn);
281 boolean containsgn2=cantremove.contains(gn2);
286 Set cycle=GraphNode.findcycles(cantremove);
287 if (cycle.contains(gn2)) {
288 if (!mustremove.contains(gn2)) {
294 cantremove.remove(gn);
296 cantremove.remove(gn2);
300 /* Searches individual conjunctions + abstract action +updates for cycles */
301 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
302 GraphNode gn=(GraphNode)it.next();
303 boolean foundnocycle=false;
305 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
306 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
307 GraphNode gn2=e.getTarget();
308 TermNode tn2=(TermNode)gn2.getOwner();
309 if (tn2.getType()!=TermNode.ABSTRACT)
311 AbstractRepair ar=tn2.getAbstract();
312 boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
313 int numadd=0;int numremove=0;
315 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
316 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
317 GraphNode gn3=e2.getTarget();
318 TermNode tn3=(TermNode)gn3.getOwner();
319 if (tn3.getType()!=TermNode.UPDATE)
322 boolean containsgn=cantremove.contains(gn);
323 boolean containsgn2=cantremove.contains(gn2);
324 boolean containsgn3=cantremove.contains(gn3);
328 Set cycle=GraphNode.findcycles(cantremove);
329 if (cycle.contains(gn3)) {
330 if (!mustremove.contains(gn3)) {
335 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
338 MultUpdateNode mun=tn3.getUpdate();
339 if (mun.getType()==MultUpdateNode.ADD)
341 if (mun.getType()==MultUpdateNode.REMOVE)
346 cantremove.remove(gn);
348 cantremove.remove(gn2);
350 cantremove.remove(gn3);
352 if (ismodify&&((numadd==0)||(numremove==0))) {
353 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
354 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
355 GraphNode gn3=e2.getTarget();
356 TermNode tn3=(TermNode)gn3.getOwner();
357 if (tn3.getType()!=TermNode.UPDATE)
359 MultUpdateNode mun=tn3.getUpdate();
360 if (((mun.getType()==MultUpdateNode.ADD)||
361 (mun.getType()==MultUpdateNode.REMOVE))&&
362 (!mustremove.contains(gn3)))
369 if (!mustremove.contains(gn)) {
376 /* Searches scope nodes + compensation nodes */
377 for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
378 GraphNode gn=(GraphNode)it.next();
380 if (nodes.contains(gn)) {
381 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
382 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
383 GraphNode gn2=e.getTarget();
384 TermNode tn2=(TermNode)gn2.getOwner();
386 if ((tn2.getType()==TermNode.CONSEQUENCE)&&
387 !mustremove.contains(gn2))
391 if (tn2.getType()!=TermNode.UPDATE)
393 /* We have a compensation node */
394 boolean containsgn=cantremove.contains(gn);
395 boolean containsgn2=cantremove.contains(gn2);
399 Set cycle=GraphNode.findcycles(cantremove);
400 if (cycle.contains(gn2)) {
401 if (!mustremove.contains(gn2)) {
406 if (!mustremove.contains(gn2))
410 cantremove.remove(gn);
412 cantremove.remove(gn2);
416 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
417 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
418 GraphNode gn2=e.getTarget();
419 TermNode tn2=(TermNode)gn2.getOwner();
420 if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
421 !mustremove.contains(gn2)) {
422 if (!cantremove.contains(gn2)) {
431 couldremove.removeAll(mustremove);
432 couldremove.removeAll(cantremove);
434 Vector couldremovevector=new Vector();
435 couldremovevector.addAll(couldremove);
436 Vector combination=new Vector();
438 continue; //recalculate
441 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
442 } catch (Exception e) {
448 GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
449 } catch (Exception e) {
454 System.out.println("Searching set of "+couldremove.size()+" nodes.");
455 System.out.println("Eliminated must "+mustremove.size()+" nodes");
456 System.out.println("Eliminated cant "+cantremove.size()+" nodes");
457 System.out.println("Searching following set:");
458 for(Iterator it=couldremove.iterator();it.hasNext();) {
459 GraphNode gn=(GraphNode)it.next();
460 System.out.println(gn.getTextLabel());
462 System.out.println("Must remove set:");
463 for(Iterator it=mustremove.iterator();it.hasNext();) {
464 GraphNode gn=(GraphNode)it.next();
465 System.out.println(gn.getTextLabel());
467 System.out.println("Cant remove set:");
468 for(Iterator it=cantremove.iterator();it.hasNext();) {
469 GraphNode gn=(GraphNode)it.next();
470 System.out.println(gn.getTextLabel());
475 if (illegal(combination,couldremovevector))
477 Set combinationset=buildset(combination,couldremovevector);
478 checkmodify(combinationset);
479 combinationset.addAll(mustremove);
480 if (combinationset!=null) {
481 System.out.println("Checkabstract="+checkAbstract(combinationset));
482 System.out.println("Checkrepairs="+checkRepairs(combinationset));
483 System.out.println("Checkall="+checkAll(combinationset));
485 if (checkAbstract(combinationset)==0&&
486 checkRepairs(combinationset)==0&&
487 checkAll(combinationset)==0) {
488 return combinationset;
491 increment(combination,couldremovevector);
493 System.out.println("Search failed!");
498 private void checkmodify(Set removednodes) {
499 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
500 GraphNode gn=(GraphNode)it.next();
501 TermNode tn=(TermNode)gn.getOwner();
502 AbstractRepair ar=tn.getAbstract();
504 /* Has MODIFYRELATION */
505 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
508 for(Iterator it2=gn.edges();it2.hasNext();) {
509 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
510 GraphNode gn2=edge.getTarget();
511 TermNode tn2=(TermNode)gn2.getOwner();
512 if (!removednodes.contains(gn2)&&
513 tn2.getType()==TermNode.UPDATE) {
514 MultUpdateNode mun=tn2.getUpdate();
516 if (mun.getType()==MultUpdateNode.ADD)
518 if (mun.getType()==MultUpdateNode.REMOVE)
522 if ((numadd==0)||(numremove==0)) {
523 for(Iterator it2=gn.edges();it2.hasNext();) {
524 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
525 GraphNode gn2=edge.getTarget();
526 TermNode tn2=(TermNode)gn2.getOwner();
527 if (!removednodes.contains(gn2)&&
528 tn2.getType()==TermNode.UPDATE) {
529 MultUpdateNode mun=tn2.getUpdate();
530 if ((mun.getType()==MultUpdateNode.ADD)
531 ||(mun.getType()==MultUpdateNode.REMOVE)) {
532 removednodes.add(gn2);
541 private static Set buildset(Vector combination, Vector couldremove) {
543 for(int i=0;i<combination.size();i++) {
544 int index=((Integer)combination.get(i)).intValue();
545 Object o=couldremove.get(index);
554 private static boolean illegal(Vector combination, Vector couldremove) {
555 if (combination.size()>couldremove.size())
559 private static void increment(Vector combination, Vector couldremove) {
560 boolean incremented=false;
561 boolean forcereset=false;
562 for(int i=0;i<combination.size();i++) {
563 int newindex=((Integer)combination.get(i)).intValue()+1;
564 if (newindex==couldremove.size()||forcereset) {
566 if ((i+1)==combination.size()) {
569 newindex=((Integer)combination.get(i+1)).intValue()+2;
570 for(int j=i;j>=0;j--) {
571 combination.set(j,new Integer(newindex));
574 if (newindex>couldremove.size())
578 combination.set(i,new Integer(newindex));
582 if (incremented==false) /* Increase length */ {
583 combination.add(new Integer(0));
584 System.out.println("Expanding to: "+combination.size());
588 /* This function checks the graph as a whole for bad cycles */
589 public int checkAll(Collection removed) {
590 Set nodes=new HashSet();
591 nodes.addAll(termination.conjunctions);
592 nodes.removeAll(removed);
593 GraphNode.computeclosure(nodes,removed);
594 Set cycles=GraphNode.findcycles(nodes);
595 for(Iterator it=cycles.iterator();it.hasNext();) {
596 GraphNode gn=(GraphNode)it.next();
597 TermNode tn=(TermNode)gn.getOwner();
598 switch(tn.getType()) {
599 case TermNode.UPDATE:
600 case TermNode.CONJUNCTION:
602 case TermNode.ABSTRACT:
603 case TermNode.RULESCOPE:
604 case TermNode.CONSEQUENCE:
612 /* This function checks that
613 1) All abstract repairs have a corresponding data structure update
615 2) All scope nodes have either a consequence node or a compensation
616 node that isn't removed.
618 public int checkRepairs(Collection removed) {
619 Set nodes=new HashSet();
620 nodes.addAll(termination.conjunctions);
621 nodes.removeAll(removed);
622 GraphNode.computeclosure(nodes,removed);
623 Set toretain=new HashSet();
624 toretain.addAll(termination.abstractrepair);
625 toretain.addAll(termination.scopenodes);
626 nodes.retainAll(toretain);
627 /* Nodes is now the reachable set of abstractrepairs */
628 /* Check to see that each has an implementation */
629 for(Iterator it=nodes.iterator();it.hasNext();) {
630 GraphNode gn=(GraphNode)it.next();
631 TermNode tn=(TermNode)gn.getOwner();
632 if (tn.getType()==TermNode.RULESCOPE) {
633 boolean foundnode=false;
634 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
635 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
636 GraphNode gn2=edge.getTarget();
637 if (!removed.contains(gn2)) {
638 TermNode tn2=(TermNode)gn2.getOwner();
639 if ((tn2.getType()==TermNode.CONSEQUENCE)||
640 (tn2.getType()==TermNode.UPDATE)) {
647 System.out.println(gn.getTextLabel());
650 } else if (tn.getType()==TermNode.ABSTRACT) {
651 boolean foundnode=false;
652 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
653 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
654 GraphNode gn2=edge.getTarget();
655 if (!removed.contains(gn2)) {
656 TermNode tn2=(TermNode)gn2.getOwner();
657 if (tn2.getType()==TermNode.UPDATE) {
665 } else throw new Error("Unanticipated Node");
669 /* This method checks that all constraints have conjunction nodes
670 and that there are no bad cycles in the abstract portion of the graph.
672 public int checkAbstract(Collection removed) {
673 Vector constraints=termination.state.vConstraints;
674 for(int i=0;i<constraints.size();i++) {
675 Constraint c=(Constraint)constraints.get(i);
676 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
678 boolean foundrepair=false;
679 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
680 GraphNode gn=(GraphNode)it.next();
681 if (!removed.contains(gn)) {
690 Set abstractnodes=new HashSet();
691 abstractnodes.addAll(termination.conjunctions);
692 abstractnodes.removeAll(removed);
693 GraphNode.computeclosure(abstractnodes,removed);
695 Set tset=new HashSet();
696 tset.addAll(termination.conjunctions);
697 tset.addAll(termination.abstractrepair);
698 tset.addAll(termination.scopenodes);
699 tset.addAll(termination.consequencenodes);
700 abstractnodes.retainAll(tset);
701 Set cycles=GraphNode.findcycles(abstractnodes);
703 for(Iterator it=cycles.iterator();it.hasNext();) {
704 GraphNode gn=(GraphNode)it.next();
705 System.out.println("NODE: "+gn.getTextLabel());
706 TermNode tn=(TermNode)gn.getOwner();
707 switch(tn.getType()) {
708 case TermNode.CONJUNCTION:
709 case TermNode.ABSTRACT:
711 case TermNode.UPDATE:
712 throw new Error("No Update Nodes should be here");