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();
23 while(!workset.empty()) {
24 GraphNode gn2=(GraphNode)workset.pop();
25 if (!closureset.contains(gn2)) {
27 boolean goodoption=false;
28 for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
29 GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
30 if (removed.contains(gn3))
32 if (termination.abstractrepair.contains(gn3)||
33 termination.conjunctions.contains(gn3)||
34 termination.updatenodes.contains(gn3))
36 if (!removed.contains(gn3)&&
37 ((!couldremove.contains(gn3))||cantremove.contains(gn3)))
42 if (termination.scopenodes.contains(gn2))
50 public Set doAnalysis() {
51 HashSet cantremove=new HashSet();
52 HashSet mustremove=new HashSet();
54 cantremove.addAll(termination.scopenodes);
55 cantremove.addAll(termination.abstractrepair);
59 HashSet nodes=new HashSet();
60 nodes.addAll(termination.conjunctions);
61 nodes.removeAll(mustremove);
62 GraphNode.computeclosure(nodes,mustremove);
63 Set cycles=GraphNode.findcycles(nodes);
64 Set couldremove=new HashSet();
65 couldremove.addAll(termination.conjunctions);
66 couldremove.addAll(termination.updatenodes);
67 couldremove.addAll(termination.consequencenodes);
68 couldremove.retainAll(nodes);
71 /* Check for consequence nodes which are fine */
73 for(Iterator it=termination.consequencenodes.iterator();it.hasNext();) {
74 GraphNode gn=(GraphNode) it.next();
75 if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
76 couldremove.remove(gn);
80 /* Check for update nodes which are fine */
82 for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
83 GraphNode gn=(GraphNode) it.next();
84 if (safetransclosure(gn, mustremove,cantremove, cantremove)) {
85 couldremove.remove(gn);
89 /* Look for constraints which can only be satisfied one way */
91 Vector constraints=termination.state.vConstraints;
92 for(int i=0;i<constraints.size();i++) {
93 Constraint c=(Constraint)constraints.get(i);
94 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
95 HashSet tmpset=new HashSet();
96 tmpset.addAll(conjunctionset);
97 tmpset.removeAll(mustremove);
98 if (tmpset.size()==1) {
99 int oldsize=cantremove.size();
100 cantremove.addAll(tmpset);
101 if (cantremove.size()!=oldsize)
107 /* Search through conjunction which must be satisfied, and attempt
108 to generate appropriate repair actions.
110 HashSet newset=new HashSet();
111 for(Iterator cit=cantremove.iterator();cit.hasNext();) {
112 GraphNode gn=(GraphNode)cit.next();
113 boolean nomodify=true;
114 HashSet toremove=new HashSet();
115 if (termination.conjunctions.contains(gn)) {
116 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
117 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
118 GraphNode gn2=e.getTarget();
119 TermNode tn2=(TermNode)gn2.getOwner();
120 if (nodes.contains(gn2)&&
121 tn2.getType()==TermNode.ABSTRACT) {
123 HashSet updateset=new HashSet();
124 for(Iterator upit=gn2.edges();upit.hasNext();) {
125 GraphNode.Edge e2=(GraphNode.Edge)upit.next();
126 GraphNode gn3=e2.getTarget();
127 TermNode tn3=(TermNode)gn3.getOwner();
128 if (tn3.getType()==TermNode.UPDATE)
131 updateset.removeAll(mustremove);
132 if (updateset.size()==1)
133 toremove.addAll(updateset);
136 newset.addAll(toremove);
141 int oldsize=cantremove.size();
142 cantremove.addAll(newset);
143 if (cantremove.size()!=oldsize)
147 /* Look for required actions for scope nodes */
148 for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
149 GraphNode gn=(GraphNode)scopeit.next();
150 HashSet tmpset=new HashSet();
151 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
152 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
153 tmpset.add(e.getTarget());
155 tmpset.removeAll(mustremove);
156 if (tmpset.size()==1) {
157 int oldsize=cantremove.size();
158 cantremove.addAll(tmpset);
159 if (cantremove.size()!=oldsize)
164 if (Compiler.AGGRESSIVESEARCH) {
165 /* Aggressively remove compensation nodes */
166 for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
167 GraphNode gn=(GraphNode)scopeit.next();
168 HashSet tmpset=new HashSet();
169 boolean doremove=false;
170 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
171 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
172 GraphNode gn2=e.getTarget();
173 if (termination.consequencenodes.contains(gn2)) {
174 if (((!couldremove.contains(gn2))||cantremove.contains(gn2))&&
175 !mustremove.contains(gn2)) {
179 } else tmpset.add(gn2);
182 mustremove.addAll(tmpset);
186 Set cycles2=GraphNode.findcycles(cantremove);
187 for(Iterator it=cycles2.iterator();it.hasNext();) {
188 GraphNode gn=(GraphNode)it.next();
189 if (termination.conjunctions.contains(gn)) {
191 GraphNode.DOTVisitor.visit(new FileOutputStream("graphdebug.dot"),cantremove);
192 } catch (Exception e) {
197 System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
198 return null; // Out of luck
202 /* Search through abstract repair actions & correspond data structure updates */
203 for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
204 GraphNode gn=(GraphNode)it.next();
205 TermNode tn=(TermNode)gn.getOwner();
207 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
208 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
209 GraphNode gn2=e.getTarget();
210 TermNode tn2=(TermNode)gn2.getOwner();
211 if (tn2.getType()!=TermNode.UPDATE)
214 boolean containsgn=cantremove.contains(gn);
215 boolean containsgn2=cantremove.contains(gn2);
220 Set cycle=GraphNode.findcycles(cantremove);
221 if (cycle.contains(gn2)) {
222 if (!mustremove.contains(gn2)) {
228 cantremove.remove(gn);
230 cantremove.remove(gn2);
234 /* Searches individual conjunctions + abstract action +updates for cycles */
235 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
236 GraphNode gn=(GraphNode)it.next();
237 boolean foundnocycle=false;
239 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
240 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
241 GraphNode gn2=e.getTarget();
242 TermNode tn2=(TermNode)gn2.getOwner();
243 if (tn2.getType()!=TermNode.ABSTRACT)
245 AbstractRepair ar=tn2.getAbstract();
246 boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
247 int numadd=0;int numremove=0;
249 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
250 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
251 GraphNode gn3=e2.getTarget();
252 TermNode tn3=(TermNode)gn3.getOwner();
253 if (tn3.getType()!=TermNode.UPDATE)
256 boolean containsgn=cantremove.contains(gn);
257 boolean containsgn2=cantremove.contains(gn2);
258 boolean containsgn3=cantremove.contains(gn3);
262 Set cycle=GraphNode.findcycles(cantremove);
263 if (cycle.contains(gn3)) {
264 if (!mustremove.contains(gn3)) {
269 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
272 MultUpdateNode mun=tn3.getUpdate();
273 if (mun.getType()==MultUpdateNode.ADD)
275 if (mun.getType()==MultUpdateNode.REMOVE)
280 cantremove.remove(gn);
282 cantremove.remove(gn2);
284 cantremove.remove(gn3);
286 if (ismodify&&((numadd==0)||(numremove==0))) {
287 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
288 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
289 GraphNode gn3=e2.getTarget();
290 TermNode tn3=(TermNode)gn3.getOwner();
291 if (tn3.getType()!=TermNode.UPDATE)
293 MultUpdateNode mun=tn3.getUpdate();
294 if (((mun.getType()==MultUpdateNode.ADD)||
295 (mun.getType()==MultUpdateNode.REMOVE))&&
296 (!mustremove.contains(gn3)))
303 if (!mustremove.contains(gn)) {
310 /* Searches scope nodes + compensation nodes */
311 for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
312 GraphNode gn=(GraphNode)it.next();
314 if (nodes.contains(gn)) {
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();
320 if ((tn2.getType()==TermNode.CONSEQUENCE)&&
321 !mustremove.contains(gn2))
325 if (tn2.getType()!=TermNode.UPDATE)
327 /* We have a compensation node */
328 boolean containsgn=cantremove.contains(gn);
329 boolean containsgn2=cantremove.contains(gn2);
333 Set cycle=GraphNode.findcycles(cantremove);
334 if (cycle.contains(gn2)) {
335 if (!mustremove.contains(gn2)) {
340 if (!mustremove.contains(gn2))
344 cantremove.remove(gn);
346 cantremove.remove(gn2);
350 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
351 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
352 GraphNode gn2=e.getTarget();
353 TermNode tn2=(TermNode)gn2.getOwner();
354 if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
355 !mustremove.contains(gn2)) {
356 if (!cantremove.contains(gn2)) {
365 couldremove.removeAll(mustremove);
366 couldremove.removeAll(cantremove);
368 Vector couldremovevector=new Vector();
369 couldremovevector.addAll(couldremove);
370 Vector combination=new Vector();
372 continue; //recalculate
375 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes,couldremove);
376 } catch (Exception e) {
381 System.out.println("Searching set of "+couldremove.size()+" nodes.");
382 System.out.println("Eliminated must "+mustremove.size()+" nodes");
383 System.out.println("Eliminated cant "+cantremove.size()+" nodes");
384 System.out.println("Searching following set:");
385 for(Iterator it=couldremove.iterator();it.hasNext();) {
386 GraphNode gn=(GraphNode)it.next();
387 System.out.println(gn.getTextLabel());
389 System.out.println("Must remove set:");
390 for(Iterator it=mustremove.iterator();it.hasNext();) {
391 GraphNode gn=(GraphNode)it.next();
392 System.out.println(gn.getTextLabel());
394 System.out.println("Cant remove set:");
395 for(Iterator it=cantremove.iterator();it.hasNext();) {
396 GraphNode gn=(GraphNode)it.next();
397 System.out.println(gn.getTextLabel());
402 if (illegal(combination,couldremovevector))
404 Set combinationset=buildset(combination,couldremovevector);
405 checkmodify(combinationset);
406 combinationset.addAll(mustremove);
407 if (combinationset!=null) {
408 System.out.println("Checkabstract="+checkAbstract(combinationset));
409 System.out.println("Checkrepairs="+checkRepairs(combinationset));
410 System.out.println("Checkall="+checkAll(combinationset));
412 if (checkAbstract(combinationset)==0&&
413 checkRepairs(combinationset)==0&&
414 checkAll(combinationset)==0) {
415 return combinationset;
418 increment(combination,couldremovevector);
420 System.out.println("Search failed!");
425 private void checkmodify(Set removednodes) {
426 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
427 GraphNode gn=(GraphNode)it.next();
428 TermNode tn=(TermNode)gn.getOwner();
429 AbstractRepair ar=tn.getAbstract();
431 /* Has MODIFYRELATION */
432 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
435 for(Iterator it2=gn.edges();it2.hasNext();) {
436 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
437 GraphNode gn2=edge.getTarget();
438 TermNode tn2=(TermNode)gn2.getOwner();
439 if (!removednodes.contains(gn2)&&
440 tn2.getType()==TermNode.UPDATE) {
441 MultUpdateNode mun=tn2.getUpdate();
443 if (mun.getType()==MultUpdateNode.ADD)
445 if (mun.getType()==MultUpdateNode.REMOVE)
449 if ((numadd==0)||(numremove==0)) {
450 for(Iterator it2=gn.edges();it2.hasNext();) {
451 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
452 GraphNode gn2=edge.getTarget();
453 TermNode tn2=(TermNode)gn2.getOwner();
454 if (!removednodes.contains(gn2)&&
455 tn2.getType()==TermNode.UPDATE) {
456 MultUpdateNode mun=tn2.getUpdate();
457 if ((mun.getType()==MultUpdateNode.ADD)
458 ||(mun.getType()==MultUpdateNode.REMOVE)) {
459 removednodes.add(gn2);
468 private static Set buildset(Vector combination, Vector couldremove) {
470 for(int i=0;i<combination.size();i++) {
471 int index=((Integer)combination.get(i)).intValue();
472 Object o=couldremove.get(index);
481 private static boolean illegal(Vector combination, Vector couldremove) {
482 if (combination.size()>couldremove.size())
486 private static void increment(Vector combination, Vector couldremove) {
487 boolean incremented=false;
488 boolean forcereset=false;
489 for(int i=0;i<combination.size();i++) {
490 int newindex=((Integer)combination.get(i)).intValue()+1;
491 if (newindex==couldremove.size()||forcereset) {
493 if ((i+1)==combination.size()) {
496 newindex=((Integer)combination.get(i+1)).intValue()+2;
497 for(int j=i;j>=0;j--) {
498 combination.set(j,new Integer(newindex));
501 if (newindex>couldremove.size())
505 combination.set(i,new Integer(newindex));
509 if (incremented==false) /* Increase length */ {
510 combination.add(new Integer(0));
511 System.out.println("Expanding to: "+combination.size());
515 /* This function checks the graph as a whole for bad cycles */
516 public int checkAll(Collection removed) {
517 Set nodes=new HashSet();
518 nodes.addAll(termination.conjunctions);
519 nodes.removeAll(removed);
520 GraphNode.computeclosure(nodes,removed);
521 Set cycles=GraphNode.findcycles(nodes);
522 for(Iterator it=cycles.iterator();it.hasNext();) {
523 GraphNode gn=(GraphNode)it.next();
524 TermNode tn=(TermNode)gn.getOwner();
525 switch(tn.getType()) {
526 case TermNode.UPDATE:
527 case TermNode.CONJUNCTION:
529 case TermNode.ABSTRACT:
530 case TermNode.RULESCOPE:
531 case TermNode.CONSEQUENCE:
539 /* This function checks that
540 1) All abstract repairs have a corresponding data structure update
542 2) All scope nodes have either a consequence node or a compensation
543 node that isn't removed.
545 public int checkRepairs(Collection removed) {
546 Set nodes=new HashSet();
547 nodes.addAll(termination.conjunctions);
548 nodes.removeAll(removed);
549 GraphNode.computeclosure(nodes,removed);
550 Set toretain=new HashSet();
551 toretain.addAll(termination.abstractrepair);
552 toretain.addAll(termination.scopenodes);
553 nodes.retainAll(toretain);
554 /* Nodes is now the reachable set of abstractrepairs */
555 /* Check to see that each has an implementation */
556 for(Iterator it=nodes.iterator();it.hasNext();) {
557 GraphNode gn=(GraphNode)it.next();
558 TermNode tn=(TermNode)gn.getOwner();
559 if (tn.getType()==TermNode.RULESCOPE) {
560 boolean foundnode=false;
561 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
562 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
563 GraphNode gn2=edge.getTarget();
564 if (!removed.contains(gn2)) {
565 TermNode tn2=(TermNode)gn2.getOwner();
566 if ((tn2.getType()==TermNode.CONSEQUENCE)||
567 (tn2.getType()==TermNode.UPDATE)) {
574 System.out.println(gn.getTextLabel());
577 } else if (tn.getType()==TermNode.ABSTRACT) {
578 boolean foundnode=false;
579 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
580 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
581 GraphNode gn2=edge.getTarget();
582 if (!removed.contains(gn2)) {
583 TermNode tn2=(TermNode)gn2.getOwner();
584 if (tn2.getType()==TermNode.UPDATE) {
592 } else throw new Error("Unanticipated Node");
596 /* This method checks that all constraints have conjunction nodes
597 and that there are no bad cycles in the abstract portion of the graph.
599 public int checkAbstract(Collection removed) {
600 Vector constraints=termination.state.vConstraints;
601 for(int i=0;i<constraints.size();i++) {
602 Constraint c=(Constraint)constraints.get(i);
603 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
605 boolean foundrepair=false;
606 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
607 GraphNode gn=(GraphNode)it.next();
608 if (!removed.contains(gn)) {
617 Set abstractnodes=new HashSet();
618 abstractnodes.addAll(termination.conjunctions);
619 abstractnodes.removeAll(removed);
620 GraphNode.computeclosure(abstractnodes,removed);
622 Set tset=new HashSet();
623 tset.addAll(termination.conjunctions);
624 tset.addAll(termination.abstractrepair);
625 tset.addAll(termination.scopenodes);
626 tset.addAll(termination.consequencenodes);
627 abstractnodes.retainAll(tset);
628 Set cycles=GraphNode.findcycles(abstractnodes);
630 for(Iterator it=cycles.iterator();it.hasNext();) {
631 GraphNode gn=(GraphNode)it.next();
632 System.out.println("NODE: "+gn.getTextLabel());
633 TermNode tn=(TermNode)gn.getOwner();
634 switch(tn.getType()) {
635 case TermNode.CONJUNCTION:
636 case TermNode.ABSTRACT:
638 case TermNode.UPDATE:
639 throw new Error("No Update Nodes should be here");