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 dependent=new HashSet();
25 /* Compute dependent set */
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))
33 if (!termination.conjunctions.contains(gn3)&&!dependent.contains(gn3)) {
40 /* Compute the closure set */
42 while(!workset.empty()) {
43 GraphNode gn2=(GraphNode)workset.pop();
44 if (!closureset.contains(gn2)) {
46 for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
47 GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
48 if (removed.contains(gn3))
55 /* Check for harmful cycles through gn */
56 Set cycles=GraphNode.findcycles(closureset);
57 if (cycles.contains(gn))
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))
70 /* Make sure all abstractrepairs/consequence nodes in the dependent nodes
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;
81 if (termination.abstractrepair.contains(gn2)&&
82 ((TermNode)gn2.getOwner()).getAbstract().getType()==AbstractRepair.MODIFYRELATION)
86 for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
87 GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
88 if (removed.contains(gn3))
90 if (cantremove.contains(gn3)||
91 !couldremove.contains(gn3)) {
93 TermNode tn3=(TermNode)gn3.getOwner();
94 MultUpdateNode mun=tn3.getUpdate();
95 if (mun.getType()==MultUpdateNode.ADD)
97 if (mun.getType()==MultUpdateNode.REMOVE)
99 if (mun.getType()==MultUpdateNode.MODIFY)
101 if ((numadd>0)&&(numremove>0||!((TermNode)gn2.getOwner()).getAbstract().needsRemoves(termination.state)))
104 if (termination.consequence.contains(gn3)||
105 termination.updatenodes.contains(gn3))
115 public Set doAnalysis() {
116 HashSet cantremove=new HashSet();
117 HashSet mustremove=new HashSet();
119 cantremove.addAll(termination.scopenodes);
120 cantremove.addAll(termination.abstractrepair);
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);
136 /* Check for consequence nodes which are fine */
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);
145 /* Check for update nodes which are fine */
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);
154 /* Check for conjunction nodes which are fine */
156 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
157 GraphNode gn=(GraphNode) it.next();
158 if (mustremove.contains(gn)||cantremove.contains(gn))
160 if (!safetransclosure(gn, mustremove,cantremove, couldremove))
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)
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());
198 /* Look for constraints which can only be satisfied one way */
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)
216 /* Search through conjunction nodes which must be
217 satisfied, and see if there are any data structure
218 updates that must exist. */
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) {
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)
241 updateset.removeAll(mustremove);
242 if (updateset.size()==1)
243 toremove.addAll(updateset);
246 newset.addAll(toremove);
251 int oldsize=cantremove.size();
252 cantremove.addAll(newset);
253 if (cantremove.size()!=oldsize)
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());
265 tmpset.removeAll(mustremove);
266 if (tmpset.size()==1) {
267 int oldsize=cantremove.size();
268 cantremove.addAll(tmpset);
269 if (cantremove.size()!=oldsize)
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)) {
289 } else tmpset.add(gn2);
292 mustremove.addAll(tmpset);
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)) {
301 GraphNode.DOTVisitor.visit(new FileOutputStream("graphdebug.dot"),cantremove);
302 } catch (Exception e) {
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());
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());
318 return null; // Out of luck
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();
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)
334 boolean containsgn=cantremove.contains(gn);
335 boolean containsgn2=cantremove.contains(gn2);
340 Set cycle=GraphNode.findcycles(cantremove);
341 if (cycle.contains(gn2)) {
342 if (!mustremove.contains(gn2)) {
348 cantremove.remove(gn);
350 cantremove.remove(gn2);
354 /* Searches individual conjunctions + abstract action +updates for cycles */
355 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
356 GraphNode gn=(GraphNode)it.next();
358 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
359 boolean foundnocycle=false;
361 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
362 GraphNode gn2=e.getTarget();
363 TermNode tn2=(TermNode)gn2.getOwner();
364 if (tn2.getType()!=TermNode.ABSTRACT)
366 AbstractRepair ar=tn2.getAbstract();
367 boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
368 int numadd=0;int numremove=0;
370 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
371 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
372 GraphNode gn3=e2.getTarget();
373 TermNode tn3=(TermNode)gn3.getOwner();
374 if (tn3.getType()!=TermNode.UPDATE)
377 boolean containsgn=cantremove.contains(gn);
378 boolean containsgn2=cantremove.contains(gn2);
379 boolean containsgn3=cantremove.contains(gn3);
383 Set cycle=GraphNode.findcycles(cantremove);
384 if (cycle.contains(gn3)) {
385 if (!mustremove.contains(gn3)) {
390 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
393 MultUpdateNode mun=tn3.getUpdate();
394 if (mun.getType()==MultUpdateNode.ADD)
396 if (mun.getType()==MultUpdateNode.REMOVE)
401 cantremove.remove(gn);
403 cantremove.remove(gn2);
405 cantremove.remove(gn3);
407 if (ismodify&&((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state)))) {
408 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
409 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
410 GraphNode gn3=e2.getTarget();
411 TermNode tn3=(TermNode)gn3.getOwner();
412 if (tn3.getType()!=TermNode.UPDATE)
414 MultUpdateNode mun=tn3.getUpdate();
415 if (((mun.getType()==MultUpdateNode.ADD)||
416 (mun.getType()==MultUpdateNode.REMOVE))&&
417 (!mustremove.contains(gn3)))
424 if (!mustremove.contains(gn)) {
432 /* Searches scope nodes + compensation nodes */
433 for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
434 GraphNode gn=(GraphNode)it.next();
435 if (nodes.contains(gn)) {
436 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
437 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
438 GraphNode gn2=e.getTarget();
439 TermNode tn2=(TermNode)gn2.getOwner();
441 if (tn2.getType()!=TermNode.UPDATE)
443 /* We have a compensation node */
444 boolean containsgn=cantremove.contains(gn);
445 boolean containsgn2=cantremove.contains(gn2);
449 Set cycle=GraphNode.findcycles(cantremove);
450 if (cycle.contains(gn2)) {
451 if (!mustremove.contains(gn2)) {
457 cantremove.remove(gn);
459 cantremove.remove(gn2);
463 couldremove.removeAll(mustremove);
464 couldremove.removeAll(cantremove);
466 Vector couldremovevector=new Vector();
467 couldremovevector.addAll(couldremove);
468 Vector combination=new Vector();
470 continue; //recalculate
473 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
474 } catch (Exception e) {
480 GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
481 } catch (Exception e) {
486 System.out.println("Searching set of "+couldremove.size()+" nodes.");
487 System.out.println("Eliminated must "+mustremove.size()+" nodes");
488 System.out.println("Eliminated cant "+cantremove.size()+" nodes");
489 System.out.println("Searching following set:");
490 for(Iterator it=couldremove.iterator();it.hasNext();) {
491 GraphNode gn=(GraphNode)it.next();
492 System.out.println(gn.getTextLabel());
494 System.out.println("Must remove set:");
495 for(Iterator it=mustremove.iterator();it.hasNext();) {
496 GraphNode gn=(GraphNode)it.next();
497 System.out.println(gn.getTextLabel());
499 System.out.println("Cant remove set:");
500 for(Iterator it=cantremove.iterator();it.hasNext();) {
501 GraphNode gn=(GraphNode)it.next();
502 System.out.println(gn.getTextLabel());
505 System.out.println("==================================================");
507 if (illegal(combination,couldremovevector))
509 Set combinationset=buildset(combination,couldremovevector);
510 System.out.println("---------------------------");
511 for(Iterator it=combinationset.iterator();it.hasNext();) {
512 System.out.println(((GraphNode)it.next()).getTextLabel());
514 System.out.println("---------------------------");
515 checkmodify(combinationset);
516 combinationset.addAll(mustremove);
517 if (combinationset!=null) {
518 int checkabstract=checkAbstract(combinationset);
519 int checkrep=checkRepairs(combinationset);
520 int checkall=checkAll(combinationset);
522 System.out.println("Checkabstract="+checkabstract);
523 System.out.println("Checkrepairs="+checkrep);
524 System.out.println("Checkall="+checkall);
526 if (checkabstract==0&&
529 return combinationset;
532 increment(combination,couldremovevector);
534 System.out.println("Search failed!");
539 private void checkmodify(Set removednodes) {
540 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
541 GraphNode gn=(GraphNode)it.next();
542 TermNode tn=(TermNode)gn.getOwner();
543 AbstractRepair ar=tn.getAbstract();
545 /* Has MODIFYRELATION */
546 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
549 for(Iterator it2=gn.edges();it2.hasNext();) {
550 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
551 GraphNode gn2=edge.getTarget();
552 TermNode tn2=(TermNode)gn2.getOwner();
553 if (!removednodes.contains(gn2)&&
554 tn2.getType()==TermNode.UPDATE) {
555 MultUpdateNode mun=tn2.getUpdate();
557 if (mun.getType()==MultUpdateNode.ADD)
559 if (mun.getType()==MultUpdateNode.REMOVE)
563 if ((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state))) {
564 for(Iterator it2=gn.edges();it2.hasNext();) {
565 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
566 GraphNode gn2=edge.getTarget();
567 TermNode tn2=(TermNode)gn2.getOwner();
568 if (!removednodes.contains(gn2)&&
569 tn2.getType()==TermNode.UPDATE) {
570 MultUpdateNode mun=tn2.getUpdate();
571 if ((mun.getType()==MultUpdateNode.ADD)
572 ||(mun.getType()==MultUpdateNode.REMOVE)) {
573 removednodes.add(gn2);
582 private static Set buildset(Vector combination, Vector couldremove) {
584 for(int i=0;i<combination.size();i++) {
585 int index=((Integer)combination.get(i)).intValue();
586 Object o=couldremove.get(index);
595 private static boolean illegal(Vector combination, Vector couldremove) {
596 if (combination.size()>couldremove.size())
600 private static void increment(Vector combination, Vector couldremove) {
601 boolean incremented=false;
602 boolean forcereset=false;
603 for(int i=0;i<combination.size();i++) {
604 int newindex=((Integer)combination.get(i)).intValue()+1;
605 if (newindex==couldremove.size()||forcereset) {
607 if ((i+1)==combination.size()) {
610 newindex=((Integer)combination.get(i+1)).intValue()+2;
611 for(int j=i;j>=0;j--) {
612 combination.set(j,new Integer(newindex));
615 if (newindex>couldremove.size())
619 combination.set(i,new Integer(newindex));
623 if (incremented==false) /* Increase length */ {
624 combination.add(new Integer(0));
625 System.out.println("Expanding to: "+combination.size());
629 /* This function checks the graph as a whole for bad cycles */
630 public int checkAll(Collection removed) {
631 Set nodes=new HashSet();
632 nodes.addAll(termination.conjunctions);
633 nodes.removeAll(removed);
634 GraphNode.computeclosure(nodes,removed);
635 Set cycles=GraphNode.findcycles(nodes);
636 for(Iterator it=cycles.iterator();it.hasNext();) {
637 GraphNode gn=(GraphNode)it.next();
638 TermNode tn=(TermNode)gn.getOwner();
639 switch(tn.getType()) {
640 case TermNode.UPDATE:
641 case TermNode.CONJUNCTION:
643 case TermNode.ABSTRACT:
644 case TermNode.RULESCOPE:
645 case TermNode.CONSEQUENCE:
653 /* This function checks that
654 1) All abstract repairs have a corresponding data structure update
656 2) All scope nodes have either a consequence node or a compensation
657 node that isn't removed.
659 public int checkRepairs(Collection removed) {
660 Set nodes=new HashSet();
661 nodes.addAll(termination.conjunctions);
662 nodes.removeAll(removed);
663 GraphNode.computeclosure(nodes,removed);
664 Set toretain=new HashSet();
665 toretain.addAll(termination.abstractrepair);
666 toretain.addAll(termination.scopenodes);
667 nodes.retainAll(toretain);
668 /* Nodes is now the reachable set of abstractrepairs */
669 /* Check to see that each has an implementation */
670 for(Iterator it=nodes.iterator();it.hasNext();) {
671 GraphNode gn=(GraphNode)it.next();
672 TermNode tn=(TermNode)gn.getOwner();
673 if (tn.getType()==TermNode.RULESCOPE) {
674 boolean foundnode=false;
675 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
676 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
677 GraphNode gn2=edge.getTarget();
678 if (!removed.contains(gn2)) {
679 TermNode tn2=(TermNode)gn2.getOwner();
680 if ((tn2.getType()==TermNode.CONSEQUENCE)||
681 (tn2.getType()==TermNode.UPDATE)) {
688 System.out.println(gn.getTextLabel());
691 } else if (tn.getType()==TermNode.ABSTRACT) {
692 boolean foundnode=false;
693 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
694 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
695 GraphNode gn2=edge.getTarget();
696 if (!removed.contains(gn2)) {
697 TermNode tn2=(TermNode)gn2.getOwner();
698 if (tn2.getType()==TermNode.UPDATE) {
706 } else throw new Error("Unanticipated Node");
710 /* This method checks that all constraints have conjunction nodes
711 and that there are no bad cycles in the abstract portion of the graph.
713 public int checkAbstract(Collection removed) {
714 Vector constraints=termination.state.vConstraints;
715 for(int i=0;i<constraints.size();i++) {
716 Constraint c=(Constraint)constraints.get(i);
717 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
719 boolean foundrepair=false;
720 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
721 GraphNode gn=(GraphNode)it.next();
722 if (!removed.contains(gn)) {
732 Set abstractnodes=new HashSet();
733 abstractnodes.addAll(termination.conjunctions);
734 abstractnodes.removeAll(removed);
735 GraphNode.computeclosure(abstractnodes,removed);
737 Set tset=new HashSet();
738 tset.addAll(termination.conjunctions);
739 tset.addAll(termination.abstractrepair);
740 tset.addAll(termination.scopenodes);
741 tset.addAll(termination.consequencenodes);
742 abstractnodes.retainAll(tset);
743 Set cycles=GraphNode.findcycles(abstractnodes);
745 for(Iterator it=cycles.iterator();it.hasNext();) {
746 GraphNode gn=(GraphNode)it.next();
747 System.out.println("NODE: "+gn.getTextLabel());
748 TermNode tn=(TermNode)gn.getOwner();
749 switch(tn.getType()) {
750 case TermNode.CONJUNCTION:
751 case TermNode.ABSTRACT:
753 case TermNode.UPDATE:
754 throw new Error("No Update Nodes should be here");