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) {
18 /** This method returns true if leaving node gn in the repair
19 * dependence graph will not result in cycles.
20 gn = updatenode, conjunctionnode, consequence node
22 private boolean safetransclosure(GraphNode gn, Set removed, Set cantremove, Set couldremove) {
23 Stack workset=new Stack();
24 HashSet closureset=new HashSet();
25 boolean needcyclecheck=false;
26 HashSet cantremovetrans=new HashSet();
29 /* Iterating over everything reachable from gn */
30 while(!workset.empty()) {
31 GraphNode gn2=(GraphNode)workset.pop();
33 /* Closureset is everything we've already iterated over */
34 if (!closureset.contains(gn2)) {
36 boolean goodoption=false;
37 for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
38 GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
39 if (removed.contains(gn3))
42 /* Consider only the nodes in the graph */
45 if (((cantremove.contains(gn2)||!couldremove.contains(gn2))
46 &&termination.conjunctions.contains(gn2))||
47 cantremovetrans.contains(gn2))
48 cantremovetrans.add(gn3);
50 if (termination.abstractrepair.contains(gn3)||
51 termination.conjunctions.contains(gn3)||
52 termination.updatenodes.contains(gn3)) {
53 /** Check for cycles if the graphnode can't
54 * be removed (we know we aren't introducing
55 * new things to repair). */
56 if ((!termination.abstractrepair.contains(gn3)&&
57 cantremove.contains(gn3))||
58 cantremovetrans.contains(gn3)) {
62 if ((!couldremove.contains(gn3))||cantremove.contains(gn3))
67 if (termination.scopenodes.contains(gn2))
73 Set cycles=GraphNode.findcycles(closureset);
74 for(Iterator it=cycles.iterator();it.hasNext();) {
75 GraphNode gn2=(GraphNode)it.next();
76 if (termination.abstractrepair.contains(gn2)||
77 termination.conjunctions.contains(gn2)||
78 termination.updatenodes.contains(gn2))
85 public Set doAnalysis() {
86 HashSet cantremove=new HashSet();
87 HashSet mustremove=new HashSet();
89 cantremove.addAll(termination.scopenodes);
90 cantremove.addAll(termination.abstractrepair);
94 HashSet nodes=new HashSet();
95 nodes.addAll(termination.conjunctions);
96 nodes.removeAll(mustremove);
97 GraphNode.computeclosure(nodes,mustremove);
98 Set cycles=GraphNode.findcycles(nodes);
99 Set couldremove=new HashSet();
100 couldremove.addAll(termination.conjunctions);
101 couldremove.addAll(termination.updatenodes);
102 couldremove.addAll(termination.consequencenodes);
103 couldremove.retainAll(nodes);
106 /* Check for consequence nodes which are fine */
108 for(Iterator it=termination.consequencenodes.iterator();it.hasNext();) {
109 GraphNode gn=(GraphNode) it.next();
110 if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
111 couldremove.remove(gn);
115 /* Check for update nodes which are fine */
117 for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
118 GraphNode gn=(GraphNode) it.next();
119 if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
120 couldremove.remove(gn);
124 /* Check for conjunction nodes which are fine */
126 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
127 GraphNode gn=(GraphNode) it.next();
128 if (mustremove.contains(gn)||cantremove.contains(gn))
130 if (!safetransclosure(gn, mustremove,cantremove, couldremove))
133 boolean allgood=true;
134 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
135 GraphNode gn2=((GraphNode.Edge)edgeit.next()).getTarget();
136 TermNode tn2=(TermNode)gn2.getOwner();
137 assert tn2.getType()==TermNode.ABSTRACT;
138 boolean foundupdate=false;
139 for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
140 GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();
141 if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
142 TermNode tn3=(TermNode)gn3.getOwner();
143 if (tn3.getType()==TermNode.UPDATE)
151 couldremove.remove(gn);
152 if (Compiler.PRUNEQUANTIFIERS) {
153 TermNode tn=(TermNode)gn.getOwner();
154 Constraint constr=tn.getConstraint();
155 for(Iterator consit=((Set)termination.conjunctionmap.get(constr)).iterator();consit.hasNext();) {
156 GraphNode gn4=(GraphNode)consit.next();
157 TermNode tn4=(TermNode)gn4.getOwner();
158 if (tn4.getquantifiernode()) {
159 mustremove.add(gn4); /* This node is history */
160 System.out.println("Eliminating: "+gn4.getTextLabel());
168 /* Look for constraints which can only be satisfied one way */
170 Vector constraints=termination.state.vConstraints;
171 for(int i=0;i<constraints.size();i++) {
172 Constraint c=(Constraint)constraints.get(i);
173 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
174 HashSet tmpset=new HashSet();
175 tmpset.addAll(conjunctionset);
176 tmpset.removeAll(mustremove);
177 if (tmpset.size()==1) {
178 int oldsize=cantremove.size();
179 cantremove.addAll(tmpset);
180 if (cantremove.size()!=oldsize)
186 /* Search through conjunction nodes which must be
187 satisfied, and see if there are any data structure
188 updates that must exist. */
190 HashSet newset=new HashSet();
191 for(Iterator cit=cantremove.iterator();cit.hasNext();) {
192 GraphNode gn=(GraphNode)cit.next();
193 boolean nomodify=true;
194 HashSet toremove=new HashSet();
195 if (termination.conjunctions.contains(gn)) {
196 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
197 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
198 GraphNode gn2=e.getTarget();
199 TermNode tn2=(TermNode)gn2.getOwner();
200 if (nodes.contains(gn2)&&
201 tn2.getType()==TermNode.ABSTRACT) {
203 HashSet updateset=new HashSet();
204 for(Iterator upit=gn2.edges();upit.hasNext();) {
205 GraphNode.Edge e2=(GraphNode.Edge)upit.next();
206 GraphNode gn3=e2.getTarget();
207 TermNode tn3=(TermNode)gn3.getOwner();
208 if (tn3.getType()==TermNode.UPDATE)
211 updateset.removeAll(mustremove);
212 if (updateset.size()==1)
213 toremove.addAll(updateset);
216 newset.addAll(toremove);
221 int oldsize=cantremove.size();
222 cantremove.addAll(newset);
223 if (cantremove.size()!=oldsize)
227 /* Look for required actions for scope nodes */
228 for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
229 GraphNode gn=(GraphNode)scopeit.next();
230 HashSet tmpset=new HashSet();
231 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
232 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
233 tmpset.add(e.getTarget());
235 tmpset.removeAll(mustremove);
236 if (tmpset.size()==1) {
237 int oldsize=cantremove.size();
238 cantremove.addAll(tmpset);
239 if (cantremove.size()!=oldsize)
244 if (Compiler.AGGRESSIVESEARCH) {
245 /* Aggressively remove compensation nodes */
246 for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
247 GraphNode gn=(GraphNode)scopeit.next();
248 HashSet tmpset=new HashSet();
249 boolean doremove=false;
250 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
251 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
252 GraphNode gn2=e.getTarget();
253 if (termination.consequencenodes.contains(gn2)) {
254 if (((!couldremove.contains(gn2))||cantremove.contains(gn2))&&
255 !mustremove.contains(gn2)) {
259 } else tmpset.add(gn2);
262 mustremove.addAll(tmpset);
266 Set cycles2=GraphNode.findcycles(cantremove);
267 for(Iterator it=cycles2.iterator();it.hasNext();) {
268 GraphNode gn=(GraphNode)it.next();
269 if (termination.conjunctions.contains(gn)) {
271 GraphNode.DOTVisitor.visit(new FileOutputStream("graphdebug.dot"),cantremove);
272 } catch (Exception e) {
277 System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
278 System.out.println("CANTREMOVE");
279 for(Iterator it2=cantremove.iterator();it2.hasNext();) {
280 GraphNode gn2=(GraphNode)it2.next();
281 System.out.println(gn2.getTextLabel());
283 System.out.println("MUSTREMOVE");
284 for(Iterator it2=mustremove.iterator();it2.hasNext();) {
285 GraphNode gn2=(GraphNode)it2.next();
286 System.out.println(gn2.getTextLabel());
288 return null; // Out of luck
292 /* Search through abstract repair actions & correspond data structure updates */
293 for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
294 GraphNode gn=(GraphNode)it.next();
295 TermNode tn=(TermNode)gn.getOwner();
297 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
298 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
299 GraphNode gn2=e.getTarget();
300 TermNode tn2=(TermNode)gn2.getOwner();
301 if (tn2.getType()!=TermNode.UPDATE)
304 boolean containsgn=cantremove.contains(gn);
305 boolean containsgn2=cantremove.contains(gn2);
310 Set cycle=GraphNode.findcycles(cantremove);
311 if (cycle.contains(gn2)) {
312 if (!mustremove.contains(gn2)) {
318 cantremove.remove(gn);
320 cantremove.remove(gn2);
324 /* Searches individual conjunctions + abstract action +updates for cycles */
325 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
326 GraphNode gn=(GraphNode)it.next();
327 boolean foundnocycle=false;
329 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
330 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
331 GraphNode gn2=e.getTarget();
332 TermNode tn2=(TermNode)gn2.getOwner();
333 if (tn2.getType()!=TermNode.ABSTRACT)
335 AbstractRepair ar=tn2.getAbstract();
336 boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
337 int numadd=0;int numremove=0;
339 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
340 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
341 GraphNode gn3=e2.getTarget();
342 TermNode tn3=(TermNode)gn3.getOwner();
343 if (tn3.getType()!=TermNode.UPDATE)
346 boolean containsgn=cantremove.contains(gn);
347 boolean containsgn2=cantremove.contains(gn2);
348 boolean containsgn3=cantremove.contains(gn3);
352 Set cycle=GraphNode.findcycles(cantremove);
353 if (cycle.contains(gn3)) {
354 if (!mustremove.contains(gn3)) {
359 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
362 MultUpdateNode mun=tn3.getUpdate();
363 if (mun.getType()==MultUpdateNode.ADD)
365 if (mun.getType()==MultUpdateNode.REMOVE)
370 cantremove.remove(gn);
372 cantremove.remove(gn2);
374 cantremove.remove(gn3);
376 if (ismodify&&((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state)))) {
377 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
378 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
379 GraphNode gn3=e2.getTarget();
380 TermNode tn3=(TermNode)gn3.getOwner();
381 if (tn3.getType()!=TermNode.UPDATE)
383 MultUpdateNode mun=tn3.getUpdate();
384 if (((mun.getType()==MultUpdateNode.ADD)||
385 (mun.getType()==MultUpdateNode.REMOVE))&&
386 (!mustremove.contains(gn3)))
393 if (!mustremove.contains(gn)) {
400 /* Searches scope nodes + compensation nodes */
401 for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
402 GraphNode gn=(GraphNode)it.next();
403 if (nodes.contains(gn)) {
404 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
405 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
406 GraphNode gn2=e.getTarget();
407 TermNode tn2=(TermNode)gn2.getOwner();
409 if (tn2.getType()!=TermNode.UPDATE)
411 /* We have a compensation node */
412 boolean containsgn=cantremove.contains(gn);
413 boolean containsgn2=cantremove.contains(gn2);
417 Set cycle=GraphNode.findcycles(cantremove);
418 if (cycle.contains(gn2)) {
419 if (!mustremove.contains(gn2)) {
425 cantremove.remove(gn);
427 cantremove.remove(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());
473 System.out.println("==================================================");
475 if (illegal(combination,couldremovevector))
477 Set combinationset=buildset(combination,couldremovevector);
478 System.out.println("---------------------------");
479 for(Iterator it=combinationset.iterator();it.hasNext();) {
480 System.out.println(((GraphNode)it.next()).getTextLabel());
482 System.out.println("---------------------------");
483 checkmodify(combinationset);
484 combinationset.addAll(mustremove);
485 if (combinationset!=null) {
486 int checkabstract=checkAbstract(combinationset);
487 int checkrep=checkRepairs(combinationset);
488 int checkall=checkAll(combinationset);
490 System.out.println("Checkabstract="+checkabstract);
491 System.out.println("Checkrepairs="+checkrep);
492 System.out.println("Checkall="+checkall);
494 if (checkabstract==0&&
497 return combinationset;
500 increment(combination,couldremovevector);
502 System.out.println("Search failed!");
507 private void checkmodify(Set removednodes) {
508 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
509 GraphNode gn=(GraphNode)it.next();
510 TermNode tn=(TermNode)gn.getOwner();
511 AbstractRepair ar=tn.getAbstract();
513 /* Has MODIFYRELATION */
514 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
517 for(Iterator it2=gn.edges();it2.hasNext();) {
518 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
519 GraphNode gn2=edge.getTarget();
520 TermNode tn2=(TermNode)gn2.getOwner();
521 if (!removednodes.contains(gn2)&&
522 tn2.getType()==TermNode.UPDATE) {
523 MultUpdateNode mun=tn2.getUpdate();
525 if (mun.getType()==MultUpdateNode.ADD)
527 if (mun.getType()==MultUpdateNode.REMOVE)
531 if ((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state))) {
532 for(Iterator it2=gn.edges();it2.hasNext();) {
533 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
534 GraphNode gn2=edge.getTarget();
535 TermNode tn2=(TermNode)gn2.getOwner();
536 if (!removednodes.contains(gn2)&&
537 tn2.getType()==TermNode.UPDATE) {
538 MultUpdateNode mun=tn2.getUpdate();
539 if ((mun.getType()==MultUpdateNode.ADD)
540 ||(mun.getType()==MultUpdateNode.REMOVE)) {
541 removednodes.add(gn2);
550 private static Set buildset(Vector combination, Vector couldremove) {
552 for(int i=0;i<combination.size();i++) {
553 int index=((Integer)combination.get(i)).intValue();
554 Object o=couldremove.get(index);
563 private static boolean illegal(Vector combination, Vector couldremove) {
564 if (combination.size()>couldremove.size())
568 private static void increment(Vector combination, Vector couldremove) {
569 boolean incremented=false;
570 boolean forcereset=false;
571 for(int i=0;i<combination.size();i++) {
572 int newindex=((Integer)combination.get(i)).intValue()+1;
573 if (newindex==couldremove.size()||forcereset) {
575 if ((i+1)==combination.size()) {
578 newindex=((Integer)combination.get(i+1)).intValue()+2;
579 for(int j=i;j>=0;j--) {
580 combination.set(j,new Integer(newindex));
583 if (newindex>couldremove.size())
587 combination.set(i,new Integer(newindex));
591 if (incremented==false) /* Increase length */ {
592 combination.add(new Integer(0));
593 System.out.println("Expanding to: "+combination.size());
597 /* This function checks the graph as a whole for bad cycles */
598 public int checkAll(Collection removed) {
599 Set nodes=new HashSet();
600 nodes.addAll(termination.conjunctions);
601 nodes.removeAll(removed);
602 GraphNode.computeclosure(nodes,removed);
603 Set cycles=GraphNode.findcycles(nodes);
604 for(Iterator it=cycles.iterator();it.hasNext();) {
605 GraphNode gn=(GraphNode)it.next();
606 TermNode tn=(TermNode)gn.getOwner();
607 switch(tn.getType()) {
608 case TermNode.UPDATE:
609 case TermNode.CONJUNCTION:
611 case TermNode.ABSTRACT:
612 case TermNode.RULESCOPE:
613 case TermNode.CONSEQUENCE:
621 /* This function checks that
622 1) All abstract repairs have a corresponding data structure update
624 2) All scope nodes have either a consequence node or a compensation
625 node that isn't removed.
627 public int checkRepairs(Collection removed) {
628 Set nodes=new HashSet();
629 nodes.addAll(termination.conjunctions);
630 nodes.removeAll(removed);
631 GraphNode.computeclosure(nodes,removed);
632 Set toretain=new HashSet();
633 toretain.addAll(termination.abstractrepair);
634 toretain.addAll(termination.scopenodes);
635 nodes.retainAll(toretain);
636 /* Nodes is now the reachable set of abstractrepairs */
637 /* Check to see that each has an implementation */
638 for(Iterator it=nodes.iterator();it.hasNext();) {
639 GraphNode gn=(GraphNode)it.next();
640 TermNode tn=(TermNode)gn.getOwner();
641 if (tn.getType()==TermNode.RULESCOPE) {
642 boolean foundnode=false;
643 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
644 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
645 GraphNode gn2=edge.getTarget();
646 if (!removed.contains(gn2)) {
647 TermNode tn2=(TermNode)gn2.getOwner();
648 if ((tn2.getType()==TermNode.CONSEQUENCE)||
649 (tn2.getType()==TermNode.UPDATE)) {
656 System.out.println(gn.getTextLabel());
659 } else if (tn.getType()==TermNode.ABSTRACT) {
660 boolean foundnode=false;
661 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
662 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
663 GraphNode gn2=edge.getTarget();
664 if (!removed.contains(gn2)) {
665 TermNode tn2=(TermNode)gn2.getOwner();
666 if (tn2.getType()==TermNode.UPDATE) {
674 } else throw new Error("Unanticipated Node");
678 /* This method checks that all constraints have conjunction nodes
679 and that there are no bad cycles in the abstract portion of the graph.
681 public int checkAbstract(Collection removed) {
682 Vector constraints=termination.state.vConstraints;
683 for(int i=0;i<constraints.size();i++) {
684 Constraint c=(Constraint)constraints.get(i);
685 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
687 boolean foundrepair=false;
688 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
689 GraphNode gn=(GraphNode)it.next();
690 if (!removed.contains(gn)) {
699 Set abstractnodes=new HashSet();
700 abstractnodes.addAll(termination.conjunctions);
701 abstractnodes.removeAll(removed);
702 GraphNode.computeclosure(abstractnodes,removed);
704 Set tset=new HashSet();
705 tset.addAll(termination.conjunctions);
706 tset.addAll(termination.abstractrepair);
707 tset.addAll(termination.scopenodes);
708 tset.addAll(termination.consequencenodes);
709 abstractnodes.retainAll(tset);
710 Set cycles=GraphNode.findcycles(abstractnodes);
712 for(Iterator it=cycles.iterator();it.hasNext();) {
713 GraphNode gn=(GraphNode)it.next();
714 System.out.println("NODE: "+gn.getTextLabel());
715 TermNode tn=(TermNode)gn.getOwner();
716 switch(tn.getType()) {
717 case TermNode.CONJUNCTION:
718 case TermNode.ABSTRACT:
720 case TermNode.UPDATE:
721 throw new Error("No Update Nodes should be here");