6 public class GraphAnalysis {
7 Termination termination;
8 static final int WORKS=0;
9 static final int ERR_NOREPAIR=1;
10 static final int ERR_CYCLE=2;
11 static final int ERR_RULE=3;
12 static final int ERR_ABSTRACT=4;
14 public GraphAnalysis(Termination t) {
18 public Set doAnalysis() {
19 HashSet cantremove=new HashSet();
20 HashSet mustremove=new HashSet();
21 HashSet optionalabstractrepair=new HashSet();
23 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
24 GraphNode gn=(GraphNode)it.next();
25 TermNode tn=(TermNode)gn.getOwner();
26 AbstractRepair ar=tn.getAbstract();
27 DNFPredicate dpred=ar.getPredicate();
28 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
29 if ((repairnodes.size()>1)&&
30 containsmodify(repairnodes)) {
31 optionalabstractrepair.add(gn);
35 cantremove.addAll(termination.scopenodes);
36 cantremove.addAll(termination.abstractrepair);
37 cantremove.removeAll(optionalabstractrepair);
41 HashSet nodes=new HashSet();
42 nodes.addAll(termination.conjunctions);
43 nodes.removeAll(mustremove);
44 GraphNode.computeclosure(nodes,mustremove);
45 Set cycles=GraphNode.findcycles(nodes);
46 Set couldremove=new HashSet();
47 couldremove.addAll(termination.conjunctions);
48 couldremove.addAll(termination.updatenodes);
49 couldremove.addAll(termination.consequencenodes);
50 couldremove.addAll(optionalabstractrepair);
51 couldremove.retainAll(cycles);
53 /* Look for constraints which can only be satisfied one way */
55 Vector constraints=termination.state.vConstraints;
56 for(int i=0;i<constraints.size();i++) {
57 Constraint c=(Constraint)constraints.get(i);
58 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
59 HashSet tmpset=new HashSet();
60 tmpset.addAll(conjunctionset);
61 tmpset.removeAll(mustremove);
62 if (tmpset.size()==1) {
63 int oldsize=cantremove.size();
64 cantremove.addAll(tmpset);
65 if (cantremove.size()!=oldsize)
70 /* Search through conjunction which must be satisfied, and attempt
71 to generate appropriate repair actions.
73 HashSet newset=new HashSet();
74 for(Iterator cit=cantremove.iterator();cit.hasNext();) {
75 GraphNode gn=(GraphNode)cit.next();
76 boolean nomodify=true;
77 HashSet toremove=new HashSet();
78 if (termination.conjunctions.contains(gn)) {
79 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
80 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
81 GraphNode gn2=e.getTarget();
82 TermNode tn2=(TermNode)gn2.getOwner();
83 if (nodes.contains(gn2)&&!mustremove.contains(gn2)&&
84 tn2.getType()==TermNode.ABSTRACT) {
86 HashSet updateset=new HashSet();
87 for(Iterator upit=gn2.edges();upit.hasNext();) {
88 GraphNode.Edge e2=(GraphNode.Edge)upit.next();
89 GraphNode gn3=e2.getTarget();
90 TermNode tn3=(TermNode)gn3.getOwner();
91 if (tn3.getType()==TermNode.UPDATE)
94 updateset.removeAll(mustremove);
96 AbstractRepair ar=tn2.getAbstract();
97 DNFPredicate dpred=ar.getPredicate();
98 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
99 if (repairnodes.size()>1&&
100 containsmodify(repairnodes)) {
101 /* We are modifying a relation */
102 HashSet retainednodes=new HashSet();
103 retainednodes.addAll(repairnodes);
104 retainednodes.retainAll(nodes);
106 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
107 if (updateset.size()==0) {
108 if (retainednodes.size()>1) {
111 } else return null; /* Out of luck */
113 if (updateset.size()==1&&retainednodes.size()==1)
114 toremove.addAll(updateset); /* Required update */
116 /* Addition or removal to relation */
117 assert (ar.getType()==AbstractRepair.ADDTORELATION)||(ar.getType()==AbstractRepair.REMOVEFROMRELATION);
118 if (updateset.size()==0) {
119 if (containsmodify(retainednodes)) {
120 /* Both ADD & REMOVE are no good */
121 for(Iterator it=retainednodes.iterator();it.hasNext();) {
122 GraphNode gnit=(GraphNode)it.next();
123 TermNode tnit=(TermNode)gnit.getOwner();
124 AbstractRepair arit=tnit.getAbstract();
125 if (arit.getType()!=AbstractRepair.MODIFYRELATION) {
126 mustremove.add(gnit);
131 return null; /* Out of luck */
133 if (updateset.size()==1&&retainednodes.size()==2)
134 toremove.addAll(updateset); /* Required update */
136 } else if (updateset.size()==1)
137 toremove.addAll(updateset);
140 newset.addAll(toremove);
144 int oldsize=cantremove.size();
145 cantremove.addAll(newset);
146 if (cantremove.size()!=oldsize)
150 /* Look for required actions for scope nodes */
151 for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
152 GraphNode gn=(GraphNode)scopeit.next();
153 HashSet tmpset=new HashSet();
154 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
155 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
156 tmpset.add(e.getTarget());
158 tmpset.removeAll(mustremove);
159 if (tmpset.size()==1) {
160 int oldsize=cantremove.size();
161 cantremove.addAll(tmpset);
162 if (cantremove.size()!=oldsize)
167 Set cycles2=GraphNode.findcycles(cantremove);
168 for(Iterator it=cycles2.iterator();it.hasNext();) {
169 GraphNode gn=(GraphNode)it.next();
170 if (termination.conjunctions.contains(gn))
171 return null; // Out of luck
174 /* Search through abstract repair actions & correspond data structure updates */
175 for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
176 GraphNode gn=(GraphNode)it.next();
177 TermNode tn=(TermNode)gn.getOwner();
179 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
180 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
181 GraphNode gn2=e.getTarget();
182 TermNode tn2=(TermNode)gn2.getOwner();
183 if (tn2.getType()!=TermNode.UPDATE)
186 boolean containsgn=cantremove.contains(gn);
187 boolean containsgn2=cantremove.contains(gn2);
192 Set cycle=GraphNode.findcycles(cantremove);
193 if (cycle.contains(gn2)) {
194 if (!mustremove.contains(gn2)) {
201 cantremove.remove(gn);
203 cantremove.remove(gn2);
207 /* Searches individual conjunctions + abstract action +updates for cycles */
208 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
209 GraphNode gn=(GraphNode)it.next();
210 boolean foundnocycle=false;
212 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
213 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
214 GraphNode gn2=e.getTarget();
215 TermNode tn2=(TermNode)gn2.getOwner();
216 if (tn2.getType()!=TermNode.ABSTRACT)
218 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
219 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
220 GraphNode gn3=e2.getTarget();
221 TermNode tn3=(TermNode)gn3.getOwner();
222 if (tn3.getType()!=TermNode.UPDATE)
224 boolean containsgn=cantremove.contains(gn);
225 boolean containsgn2=cantremove.contains(gn2);
226 boolean containsgn3=cantremove.contains(gn3);
230 Set cycle=GraphNode.findcycles(cantremove);
231 if (cycle.contains(gn3)) {
232 if (!mustremove.contains(gn3)) {
237 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
241 cantremove.remove(gn);
243 cantremove.remove(gn2);
245 cantremove.remove(gn3);
249 if (!mustremove.contains(gn)) {
256 /* Searches scope nodes + compensation nodes */
257 for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
258 GraphNode gn=(GraphNode)it.next();
259 boolean foundcompensation=false;
260 if (nodes.contains(gn)) {
261 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
262 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
263 GraphNode gn2=e.getTarget();
264 TermNode tn2=(TermNode)gn2.getOwner();
266 if (tn2.getType()!=TermNode.UPDATE)
268 /* We have a compensation node */
269 boolean containsgn=cantremove.contains(gn);
270 boolean containsgn2=cantremove.contains(gn2);
274 Set cycle=GraphNode.findcycles(cantremove);
275 if (cycle.contains(gn2)) {
276 if (!mustremove.contains(gn2)) {
281 if (!mustremove.contains(gn2))
282 foundcompensation=true;
285 cantremove.remove(gn);
287 cantremove.remove(gn2);
290 if (!foundcompensation) {
291 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
292 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
293 GraphNode gn2=e.getTarget();
294 TermNode tn2=(TermNode)gn2.getOwner();
295 if (tn2.getType()==TermNode.UPDATE) {
302 couldremove.removeAll(mustremove);
303 couldremove.removeAll(cantremove);
305 Vector couldremovevector=new Vector();
306 couldremovevector.addAll(couldremove);
307 Vector combination=new Vector();
309 continue; //recalculate
312 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
313 } catch (Exception e) {
318 System.out.println("Searching set of "+couldremove.size()+" nodes.");
319 System.out.println("Eliminated must "+mustremove.size()+" nodes");
320 System.out.println("Eliminated cant "+cantremove.size()+" nodes");
321 System.out.println("Searching following set:");
322 for(Iterator it=couldremove.iterator();it.hasNext();) {
323 GraphNode gn=(GraphNode)it.next();
324 System.out.println(gn.getTextLabel());
329 if (illegal(combination,couldremovevector))
331 Set combinationset=buildset(combination,couldremovevector);
332 checkmodify(combinationset);
333 combinationset.addAll(mustremove);
334 if (combinationset!=null) {
335 System.out.println("Checkabstract="+checkAbstract(combinationset));
336 System.out.println("Checkrepairs="+checkRepairs(combinationset));
337 System.out.println("Checkall="+checkAll(combinationset));
339 if (checkAbstract(combinationset)==0&&
340 checkRepairs(combinationset)==0&&
341 checkAll(combinationset)==0) {
342 return combinationset;
345 increment(combination,couldremovevector);
351 private void checkmodify(Set removednodes) {
352 for (Iterator it=removednodes.iterator();it.hasNext();) {
353 GraphNode gn=(GraphNode)it.next();
354 TermNode tn=(TermNode)gn.getOwner();
355 if (tn.getType()==TermNode.ABSTRACT) {
356 AbstractRepair ar=tn.getAbstract();
357 DNFPredicate dpred=ar.getPredicate();
358 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
359 /* Has MODIFYRELATION */
360 if (containsmodify(repairnodes)&&
361 (repairnodes.size()>1)&&
362 (ar.getType()==AbstractRepair.REMOVEFROMRELATION||
363 ar.getType()==AbstractRepair.ADDTORELATION)) {
364 for(Iterator it2=repairnodes.iterator();it2.hasNext();) {
365 GraphNode gn2=(GraphNode)it2.next();
366 TermNode tn2=(TermNode)gn2.getOwner();
367 AbstractRepair ar2=tn2.getAbstract();
368 if (ar2.getType()==AbstractRepair.REMOVEFROMRELATION||
369 ar2.getType()==AbstractRepair.ADDTORELATION) {
370 removednodes.add(gn2);
378 private static boolean containsmodify(Set repairnodes) {
379 for (Iterator it=repairnodes.iterator();it.hasNext();) {
380 GraphNode gn=(GraphNode) it.next();
381 TermNode tn=(TermNode)gn.getOwner();
382 AbstractRepair ar=tn.getAbstract();
383 if (ar.getType()==AbstractRepair.MODIFYRELATION)
389 private static Set buildset(Vector combination, Vector couldremove) {
391 for(int i=0;i<combination.size();i++) {
392 int index=((Integer)combination.get(i)).intValue();
393 Object o=couldremove.get(index);
402 private static boolean illegal(Vector combination, Vector couldremove) {
403 if (combination.size()>couldremove.size())
407 private static void increment(Vector combination, Vector couldremove) {
408 boolean incremented=false;
409 boolean forcereset=false;
410 for(int i=0;i<combination.size();i++) {
411 int newindex=((Integer)combination.get(i)).intValue()+1;
412 if (newindex==couldremove.size()||forcereset) {
414 if ((i+1)==combination.size()) {
417 newindex=((Integer)combination.get(i+1)).intValue()+2;
418 for(int j=i;j>=0;j--) {
419 combination.set(j,new Integer(newindex));
422 if (newindex>couldremove.size())
426 combination.set(i,new Integer(newindex));
430 if (incremented==false) /* Increase length */ {
431 combination.add(new Integer(0));
432 System.out.println("Expanding to :"+combination.size());
436 /* This function checks the graph as a whole for bad cycles */
437 public int checkAll(Collection removed) {
438 Set nodes=new HashSet();
439 nodes.addAll(termination.conjunctions);
440 nodes.removeAll(removed);
441 GraphNode.computeclosure(nodes,removed);
442 Set cycles=GraphNode.findcycles(nodes);
443 for(Iterator it=cycles.iterator();it.hasNext();) {
444 GraphNode gn=(GraphNode)it.next();
445 TermNode tn=(TermNode)gn.getOwner();
446 switch(tn.getType()) {
447 case TermNode.UPDATE:
448 case TermNode.CONJUNCTION:
450 case TermNode.ABSTRACT:
451 case TermNode.RULESCOPE:
452 case TermNode.CONSEQUENCE:
460 /* This function checks that
461 1) All abstract repairs have a corresponding data structure update
463 2) All scope nodes have either a consequence node or a compensation
464 node that isn't removed.
466 public int checkRepairs(Collection removed) {
467 Set nodes=new HashSet();
468 nodes.addAll(termination.conjunctions);
469 nodes.removeAll(removed);
470 GraphNode.computeclosure(nodes,removed);
471 Set toretain=new HashSet();
472 toretain.addAll(termination.abstractrepair);
473 toretain.addAll(termination.scopenodes);
474 nodes.retainAll(toretain);
475 /* Nodes is now the reachable set of abstractrepairs */
476 /* Check to see that each has an implementation */
477 for(Iterator it=nodes.iterator();it.hasNext();) {
478 GraphNode gn=(GraphNode)it.next();
479 TermNode tn=(TermNode)gn.getOwner();
480 if (tn.getType()==TermNode.RULESCOPE) {
481 boolean foundnode=false;
482 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
483 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
484 GraphNode gn2=edge.getTarget();
485 if (!removed.contains(gn2)) {
486 TermNode tn2=(TermNode)gn2.getOwner();
487 if ((tn2.getType()==TermNode.CONSEQUENCE)||
488 (tn2.getType()==TermNode.UPDATE)) {
495 System.out.println(gn.getTextLabel());
498 } else if (tn.getType()==TermNode.ABSTRACT) {
499 boolean foundnode=false;
500 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
501 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
502 GraphNode gn2=edge.getTarget();
503 if (!removed.contains(gn2)) {
504 TermNode tn2=(TermNode)gn2.getOwner();
505 if (tn2.getType()==TermNode.UPDATE) {
513 } else throw new Error("Unanticipated Node");
517 /* This method checks that all constraints have conjunction nodes
518 and that there are no bad cycles in the abstract portion of the graph.
520 public int checkAbstract(Collection removed) {
521 Vector constraints=termination.state.vConstraints;
522 for(int i=0;i<constraints.size();i++) {
523 Constraint c=(Constraint)constraints.get(i);
524 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
526 boolean foundrepair=false;
527 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
528 GraphNode gn=(GraphNode)it.next();
529 if (!removed.contains(gn)) {
531 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
532 GraphNode.Edge edge=(GraphNode.Edge) edgeit.next();
533 GraphNode gn2=edge.getTarget();
534 TermNode tn2=(TermNode) gn2.getOwner();
535 if (tn2.getType()==TermNode.ABSTRACT) {
537 AbstractRepair ar=tn2.getAbstract();
538 DNFPredicate dpred=ar.getPredicate();
539 Set repairnodes=(Set)termination.predtoabstractmap.get(dpred);
540 if (containsmodify(repairnodes)&&
541 (repairnodes.size()>1)) {
542 HashSet retainednodes=new HashSet();
543 retainednodes.addAll(repairnodes);
544 retainednodes.removeAll(removed);
545 if (!containsmodify(retainednodes)&&
546 (retainednodes.size()<2))
548 } else if (removed.contains(gn2))
557 Set abstractnodes=new HashSet();
558 abstractnodes.addAll(termination.conjunctions);
559 abstractnodes.removeAll(removed);
560 GraphNode.computeclosure(abstractnodes,removed);
562 Set tset=new HashSet();
563 tset.addAll(termination.conjunctions);
564 tset.addAll(termination.abstractrepair);
565 tset.addAll(termination.scopenodes);
566 tset.addAll(termination.consequencenodes);
567 abstractnodes.retainAll(tset);
568 Set cycles=GraphNode.findcycles(abstractnodes);
570 for(Iterator it=cycles.iterator();it.hasNext();) {
571 GraphNode gn=(GraphNode)it.next();
572 System.out.println("NODE: "+gn.getTextLabel());
573 TermNode tn=(TermNode)gn.getOwner();
574 switch(tn.getType()) {
575 case TermNode.CONJUNCTION:
576 case TermNode.ABSTRACT:
578 case TermNode.UPDATE:
579 throw new Error("No Update Nodes should be here");