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();
357 boolean foundnocycle=false;
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)
365 AbstractRepair ar=tn2.getAbstract();
366 boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
367 int numadd=0;int numremove=0;
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)
376 boolean containsgn=cantremove.contains(gn);
377 boolean containsgn2=cantremove.contains(gn2);
378 boolean containsgn3=cantremove.contains(gn3);
382 Set cycle=GraphNode.findcycles(cantremove);
383 if (cycle.contains(gn3)) {
384 if (!mustremove.contains(gn3)) {
389 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
392 MultUpdateNode mun=tn3.getUpdate();
393 if (mun.getType()==MultUpdateNode.ADD)
395 if (mun.getType()==MultUpdateNode.REMOVE)
400 cantremove.remove(gn);
402 cantremove.remove(gn2);
404 cantremove.remove(gn3);
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)
413 MultUpdateNode mun=tn3.getUpdate();
414 if (((mun.getType()==MultUpdateNode.ADD)||
415 (mun.getType()==MultUpdateNode.REMOVE))&&
416 (!mustremove.contains(gn3)))
423 if (!mustremove.contains(gn)) {
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();
439 if (tn2.getType()!=TermNode.UPDATE)
441 /* We have a compensation node */
442 boolean containsgn=cantremove.contains(gn);
443 boolean containsgn2=cantremove.contains(gn2);
447 Set cycle=GraphNode.findcycles(cantremove);
448 if (cycle.contains(gn2)) {
449 if (!mustremove.contains(gn2)) {
455 cantremove.remove(gn);
457 cantremove.remove(gn2);
461 couldremove.removeAll(mustremove);
462 couldremove.removeAll(cantremove);
464 Vector couldremovevector=new Vector();
465 couldremovevector.addAll(couldremove);
466 Vector combination=new Vector();
468 continue; //recalculate
471 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
472 } catch (Exception e) {
478 GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
479 } catch (Exception e) {
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());
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());
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());
503 System.out.println("==================================================");
505 if (illegal(combination,couldremovevector))
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());
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);
520 System.out.println("Checkabstract="+checkabstract);
521 System.out.println("Checkrepairs="+checkrep);
522 System.out.println("Checkall="+checkall);
524 if (checkabstract==0&&
527 return combinationset;
530 increment(combination,couldremovevector);
532 System.out.println("Search failed!");
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();
543 /* Has MODIFYRELATION */
544 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
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();
555 if (mun.getType()==MultUpdateNode.ADD)
557 if (mun.getType()==MultUpdateNode.REMOVE)
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);
580 private static Set buildset(Vector combination, Vector couldremove) {
582 for(int i=0;i<combination.size();i++) {
583 int index=((Integer)combination.get(i)).intValue();
584 Object o=couldremove.get(index);
593 private static boolean illegal(Vector combination, Vector couldremove) {
594 if (combination.size()>couldremove.size())
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) {
605 if ((i+1)==combination.size()) {
608 newindex=((Integer)combination.get(i+1)).intValue()+2;
609 for(int j=i;j>=0;j--) {
610 combination.set(j,new Integer(newindex));
613 if (newindex>couldremove.size())
617 combination.set(i,new Integer(newindex));
621 if (incremented==false) /* Increase length */ {
622 combination.add(new Integer(0));
623 System.out.println("Expanding to: "+combination.size());
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:
641 case TermNode.ABSTRACT:
642 case TermNode.RULESCOPE:
643 case TermNode.CONSEQUENCE:
651 /* This function checks that
652 1) All abstract repairs have a corresponding data structure update
654 2) All scope nodes have either a consequence node or a compensation
655 node that isn't removed.
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)) {
686 System.out.println(gn.getTextLabel());
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) {
704 } else throw new Error("Unanticipated Node");
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.
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);
717 boolean foundrepair=false;
718 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
719 GraphNode gn=(GraphNode)it.next();
720 if (!removed.contains(gn)) {
729 Set abstractnodes=new HashSet();
730 abstractnodes.addAll(termination.conjunctions);
731 abstractnodes.removeAll(removed);
732 GraphNode.computeclosure(abstractnodes,removed);
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);
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:
750 case TermNode.UPDATE:
751 throw new Error("No Update Nodes should be here");