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 System.out.println("CANTREMOVE");
265 for(Iterator it2=cantremove.iterator();it2.hasNext();) {
266 GraphNode gn2=(GraphNode)it2.next();
267 System.out.println(gn2.getTextLabel());
269 System.out.println("MUSTREMOVE");
270 for(Iterator it2=mustremove.iterator();it2.hasNext();) {
271 GraphNode gn2=(GraphNode)it2.next();
272 System.out.println(gn2.getTextLabel());
274 return null; // Out of luck
278 /* Search through abstract repair actions & correspond data structure updates */
279 for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
280 GraphNode gn=(GraphNode)it.next();
281 TermNode tn=(TermNode)gn.getOwner();
283 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
284 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
285 GraphNode gn2=e.getTarget();
286 TermNode tn2=(TermNode)gn2.getOwner();
287 if (tn2.getType()!=TermNode.UPDATE)
290 boolean containsgn=cantremove.contains(gn);
291 boolean containsgn2=cantremove.contains(gn2);
296 Set cycle=GraphNode.findcycles(cantremove);
297 if (cycle.contains(gn2)) {
298 if (!mustremove.contains(gn2)) {
304 cantremove.remove(gn);
306 cantremove.remove(gn2);
310 /* Searches individual conjunctions + abstract action +updates for cycles */
311 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
312 GraphNode gn=(GraphNode)it.next();
313 boolean foundnocycle=false;
315 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
316 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
317 GraphNode gn2=e.getTarget();
318 TermNode tn2=(TermNode)gn2.getOwner();
319 if (tn2.getType()!=TermNode.ABSTRACT)
321 AbstractRepair ar=tn2.getAbstract();
322 boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
323 int numadd=0;int numremove=0;
325 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
326 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
327 GraphNode gn3=e2.getTarget();
328 TermNode tn3=(TermNode)gn3.getOwner();
329 if (tn3.getType()!=TermNode.UPDATE)
332 boolean containsgn=cantremove.contains(gn);
333 boolean containsgn2=cantremove.contains(gn2);
334 boolean containsgn3=cantremove.contains(gn3);
338 Set cycle=GraphNode.findcycles(cantremove);
339 if (cycle.contains(gn3)) {
340 if (!mustremove.contains(gn3)) {
345 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
348 MultUpdateNode mun=tn3.getUpdate();
349 if (mun.getType()==MultUpdateNode.ADD)
351 if (mun.getType()==MultUpdateNode.REMOVE)
356 cantremove.remove(gn);
358 cantremove.remove(gn2);
360 cantremove.remove(gn3);
362 if (ismodify&&((numadd==0)||(numremove==0))) {
363 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
364 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
365 GraphNode gn3=e2.getTarget();
366 TermNode tn3=(TermNode)gn3.getOwner();
367 if (tn3.getType()!=TermNode.UPDATE)
369 MultUpdateNode mun=tn3.getUpdate();
370 if (((mun.getType()==MultUpdateNode.ADD)||
371 (mun.getType()==MultUpdateNode.REMOVE))&&
372 (!mustremove.contains(gn3)))
379 if (!mustremove.contains(gn)) {
386 /* Searches scope nodes + compensation nodes */
387 for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
388 GraphNode gn=(GraphNode)it.next();
390 if (nodes.contains(gn)) {
391 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
392 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
393 GraphNode gn2=e.getTarget();
394 TermNode tn2=(TermNode)gn2.getOwner();
396 if ((tn2.getType()==TermNode.CONSEQUENCE)&&
397 !mustremove.contains(gn2))
401 if (tn2.getType()!=TermNode.UPDATE)
403 /* We have a compensation node */
404 boolean containsgn=cantremove.contains(gn);
405 boolean containsgn2=cantremove.contains(gn2);
409 Set cycle=GraphNode.findcycles(cantremove);
410 if (cycle.contains(gn2)) {
411 if (!mustremove.contains(gn2)) {
416 if (!mustremove.contains(gn2))
420 cantremove.remove(gn);
422 cantremove.remove(gn2);
426 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
427 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
428 GraphNode gn2=e.getTarget();
429 TermNode tn2=(TermNode)gn2.getOwner();
430 if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
431 !mustremove.contains(gn2)) {
432 if (!cantremove.contains(gn2)) {
441 couldremove.removeAll(mustremove);
442 couldremove.removeAll(cantremove);
444 Vector couldremovevector=new Vector();
445 couldremovevector.addAll(couldremove);
446 Vector combination=new Vector();
448 continue; //recalculate
451 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
452 } catch (Exception e) {
458 GraphNode.DOTVisitor.visit(new FileOutputStream("graphcycle.dot"),GraphNode.findcycles(nodes),couldremove);
459 } catch (Exception e) {
464 System.out.println("Searching set of "+couldremove.size()+" nodes.");
465 System.out.println("Eliminated must "+mustremove.size()+" nodes");
466 System.out.println("Eliminated cant "+cantremove.size()+" nodes");
467 System.out.println("Searching following set:");
468 for(Iterator it=couldremove.iterator();it.hasNext();) {
469 GraphNode gn=(GraphNode)it.next();
470 System.out.println(gn.getTextLabel());
472 System.out.println("Must remove set:");
473 for(Iterator it=mustremove.iterator();it.hasNext();) {
474 GraphNode gn=(GraphNode)it.next();
475 System.out.println(gn.getTextLabel());
477 System.out.println("Cant remove set:");
478 for(Iterator it=cantremove.iterator();it.hasNext();) {
479 GraphNode gn=(GraphNode)it.next();
480 System.out.println(gn.getTextLabel());
485 if (illegal(combination,couldremovevector))
487 Set combinationset=buildset(combination,couldremovevector);
488 checkmodify(combinationset);
489 combinationset.addAll(mustremove);
490 if (combinationset!=null) {
491 System.out.println("Checkabstract="+checkAbstract(combinationset));
492 System.out.println("Checkrepairs="+checkRepairs(combinationset));
493 System.out.println("Checkall="+checkAll(combinationset));
495 if (checkAbstract(combinationset)==0&&
496 checkRepairs(combinationset)==0&&
497 checkAll(combinationset)==0) {
498 return combinationset;
501 increment(combination,couldremovevector);
503 System.out.println("Search failed!");
508 private void checkmodify(Set removednodes) {
509 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
510 GraphNode gn=(GraphNode)it.next();
511 TermNode tn=(TermNode)gn.getOwner();
512 AbstractRepair ar=tn.getAbstract();
514 /* Has MODIFYRELATION */
515 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
518 for(Iterator it2=gn.edges();it2.hasNext();) {
519 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
520 GraphNode gn2=edge.getTarget();
521 TermNode tn2=(TermNode)gn2.getOwner();
522 if (!removednodes.contains(gn2)&&
523 tn2.getType()==TermNode.UPDATE) {
524 MultUpdateNode mun=tn2.getUpdate();
526 if (mun.getType()==MultUpdateNode.ADD)
528 if (mun.getType()==MultUpdateNode.REMOVE)
532 if ((numadd==0)||(numremove==0)) {
533 for(Iterator it2=gn.edges();it2.hasNext();) {
534 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
535 GraphNode gn2=edge.getTarget();
536 TermNode tn2=(TermNode)gn2.getOwner();
537 if (!removednodes.contains(gn2)&&
538 tn2.getType()==TermNode.UPDATE) {
539 MultUpdateNode mun=tn2.getUpdate();
540 if ((mun.getType()==MultUpdateNode.ADD)
541 ||(mun.getType()==MultUpdateNode.REMOVE)) {
542 removednodes.add(gn2);
551 private static Set buildset(Vector combination, Vector couldremove) {
553 for(int i=0;i<combination.size();i++) {
554 int index=((Integer)combination.get(i)).intValue();
555 Object o=couldremove.get(index);
564 private static boolean illegal(Vector combination, Vector couldremove) {
565 if (combination.size()>couldremove.size())
569 private static void increment(Vector combination, Vector couldremove) {
570 boolean incremented=false;
571 boolean forcereset=false;
572 for(int i=0;i<combination.size();i++) {
573 int newindex=((Integer)combination.get(i)).intValue()+1;
574 if (newindex==couldremove.size()||forcereset) {
576 if ((i+1)==combination.size()) {
579 newindex=((Integer)combination.get(i+1)).intValue()+2;
580 for(int j=i;j>=0;j--) {
581 combination.set(j,new Integer(newindex));
584 if (newindex>couldremove.size())
588 combination.set(i,new Integer(newindex));
592 if (incremented==false) /* Increase length */ {
593 combination.add(new Integer(0));
594 System.out.println("Expanding to: "+combination.size());
598 /* This function checks the graph as a whole for bad cycles */
599 public int checkAll(Collection removed) {
600 Set nodes=new HashSet();
601 nodes.addAll(termination.conjunctions);
602 nodes.removeAll(removed);
603 GraphNode.computeclosure(nodes,removed);
604 Set cycles=GraphNode.findcycles(nodes);
605 for(Iterator it=cycles.iterator();it.hasNext();) {
606 GraphNode gn=(GraphNode)it.next();
607 TermNode tn=(TermNode)gn.getOwner();
608 switch(tn.getType()) {
609 case TermNode.UPDATE:
610 case TermNode.CONJUNCTION:
612 case TermNode.ABSTRACT:
613 case TermNode.RULESCOPE:
614 case TermNode.CONSEQUENCE:
622 /* This function checks that
623 1) All abstract repairs have a corresponding data structure update
625 2) All scope nodes have either a consequence node or a compensation
626 node that isn't removed.
628 public int checkRepairs(Collection removed) {
629 Set nodes=new HashSet();
630 nodes.addAll(termination.conjunctions);
631 nodes.removeAll(removed);
632 GraphNode.computeclosure(nodes,removed);
633 Set toretain=new HashSet();
634 toretain.addAll(termination.abstractrepair);
635 toretain.addAll(termination.scopenodes);
636 nodes.retainAll(toretain);
637 /* Nodes is now the reachable set of abstractrepairs */
638 /* Check to see that each has an implementation */
639 for(Iterator it=nodes.iterator();it.hasNext();) {
640 GraphNode gn=(GraphNode)it.next();
641 TermNode tn=(TermNode)gn.getOwner();
642 if (tn.getType()==TermNode.RULESCOPE) {
643 boolean foundnode=false;
644 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
645 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
646 GraphNode gn2=edge.getTarget();
647 if (!removed.contains(gn2)) {
648 TermNode tn2=(TermNode)gn2.getOwner();
649 if ((tn2.getType()==TermNode.CONSEQUENCE)||
650 (tn2.getType()==TermNode.UPDATE)) {
657 System.out.println(gn.getTextLabel());
660 } else if (tn.getType()==TermNode.ABSTRACT) {
661 boolean foundnode=false;
662 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
663 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
664 GraphNode gn2=edge.getTarget();
665 if (!removed.contains(gn2)) {
666 TermNode tn2=(TermNode)gn2.getOwner();
667 if (tn2.getType()==TermNode.UPDATE) {
675 } else throw new Error("Unanticipated Node");
679 /* This method checks that all constraints have conjunction nodes
680 and that there are no bad cycles in the abstract portion of the graph.
682 public int checkAbstract(Collection removed) {
683 Vector constraints=termination.state.vConstraints;
684 for(int i=0;i<constraints.size();i++) {
685 Constraint c=(Constraint)constraints.get(i);
686 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
688 boolean foundrepair=false;
689 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
690 GraphNode gn=(GraphNode)it.next();
691 if (!removed.contains(gn)) {
700 Set abstractnodes=new HashSet();
701 abstractnodes.addAll(termination.conjunctions);
702 abstractnodes.removeAll(removed);
703 GraphNode.computeclosure(abstractnodes,removed);
705 Set tset=new HashSet();
706 tset.addAll(termination.conjunctions);
707 tset.addAll(termination.abstractrepair);
708 tset.addAll(termination.scopenodes);
709 tset.addAll(termination.consequencenodes);
710 abstractnodes.retainAll(tset);
711 Set cycles=GraphNode.findcycles(abstractnodes);
713 for(Iterator it=cycles.iterator();it.hasNext();) {
714 GraphNode gn=(GraphNode)it.next();
715 System.out.println("NODE: "+gn.getTextLabel());
716 TermNode tn=(TermNode)gn.getOwner();
717 switch(tn.getType()) {
718 case TermNode.CONJUNCTION:
719 case TermNode.ABSTRACT:
721 case TermNode.UPDATE:
722 throw new Error("No Update Nodes should be here");