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();
22 cantremove.addAll(termination.scopenodes);
23 cantremove.addAll(termination.abstractrepair);
27 HashSet nodes=new HashSet();
28 nodes.addAll(termination.conjunctions);
29 nodes.removeAll(mustremove);
30 GraphNode.computeclosure(nodes,mustremove);
31 Set cycles=GraphNode.findcycles(nodes);
32 Set couldremove=new HashSet();
33 couldremove.addAll(termination.conjunctions);
34 couldremove.addAll(termination.updatenodes);
35 couldremove.addAll(termination.consequencenodes);
36 couldremove.retainAll(nodes);
38 /* Look for constraints which can only be satisfied one way */
40 Vector constraints=termination.state.vConstraints;
41 for(int i=0;i<constraints.size();i++) {
42 Constraint c=(Constraint)constraints.get(i);
43 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
44 HashSet tmpset=new HashSet();
45 tmpset.addAll(conjunctionset);
46 tmpset.removeAll(mustremove);
47 if (tmpset.size()==1) {
48 int oldsize=cantremove.size();
49 cantremove.addAll(tmpset);
50 if (cantremove.size()!=oldsize)
56 /* Search through conjunction which must be satisfied, and attempt
57 to generate appropriate repair actions.
59 HashSet newset=new HashSet();
60 for(Iterator cit=cantremove.iterator();cit.hasNext();) {
61 GraphNode gn=(GraphNode)cit.next();
62 boolean nomodify=true;
63 HashSet toremove=new HashSet();
64 if (termination.conjunctions.contains(gn)) {
65 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
66 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
67 GraphNode gn2=e.getTarget();
68 TermNode tn2=(TermNode)gn2.getOwner();
69 if (nodes.contains(gn2)&&
70 tn2.getType()==TermNode.ABSTRACT) {
72 HashSet updateset=new HashSet();
73 for(Iterator upit=gn2.edges();upit.hasNext();) {
74 GraphNode.Edge e2=(GraphNode.Edge)upit.next();
75 GraphNode gn3=e2.getTarget();
76 TermNode tn3=(TermNode)gn3.getOwner();
77 if (tn3.getType()==TermNode.UPDATE)
80 updateset.removeAll(mustremove);
81 if (updateset.size()==1)
82 toremove.addAll(updateset);
85 newset.addAll(toremove);
90 int oldsize=cantremove.size();
91 cantremove.addAll(newset);
92 if (cantremove.size()!=oldsize)
96 /* Look for required actions for scope nodes */
97 for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
98 GraphNode gn=(GraphNode)scopeit.next();
99 HashSet tmpset=new HashSet();
100 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
101 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
102 tmpset.add(e.getTarget());
104 tmpset.removeAll(mustremove);
105 if (tmpset.size()==1) {
106 int oldsize=cantremove.size();
107 cantremove.addAll(tmpset);
108 if (cantremove.size()!=oldsize)
113 Set cycles2=GraphNode.findcycles(cantremove);
114 for(Iterator it=cycles2.iterator();it.hasNext();) {
115 GraphNode gn=(GraphNode)it.next();
116 if (termination.conjunctions.contains(gn)) {
118 GraphNode.DOTVisitor.visit(new FileOutputStream("graphdebug.dot"),cantremove);
119 } catch (Exception e) {
124 System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
125 return null; // Out of luck
129 /* Search through abstract repair actions & correspond data structure updates */
130 for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
131 GraphNode gn=(GraphNode)it.next();
132 TermNode tn=(TermNode)gn.getOwner();
134 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
135 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
136 GraphNode gn2=e.getTarget();
137 TermNode tn2=(TermNode)gn2.getOwner();
138 if (tn2.getType()!=TermNode.UPDATE)
141 boolean containsgn=cantremove.contains(gn);
142 boolean containsgn2=cantremove.contains(gn2);
147 Set cycle=GraphNode.findcycles(cantremove);
148 if (cycle.contains(gn2)) {
149 if (!mustremove.contains(gn2)) {
155 cantremove.remove(gn);
157 cantremove.remove(gn2);
161 /* Searches individual conjunctions + abstract action +updates for cycles */
162 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
163 GraphNode gn=(GraphNode)it.next();
164 boolean foundnocycle=false;
166 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
167 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
168 GraphNode gn2=e.getTarget();
169 TermNode tn2=(TermNode)gn2.getOwner();
170 if (tn2.getType()!=TermNode.ABSTRACT)
172 AbstractRepair ar=tn2.getAbstract();
173 boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
174 int numadd=0;int numremove=0;
176 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
177 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
178 GraphNode gn3=e2.getTarget();
179 TermNode tn3=(TermNode)gn3.getOwner();
180 if (tn3.getType()!=TermNode.UPDATE)
183 boolean containsgn=cantremove.contains(gn);
184 boolean containsgn2=cantremove.contains(gn2);
185 boolean containsgn3=cantremove.contains(gn3);
189 Set cycle=GraphNode.findcycles(cantremove);
190 if (cycle.contains(gn3)) {
191 if (!mustremove.contains(gn3)) {
196 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
199 MultUpdateNode mun=tn3.getUpdate();
200 if (mun.getType()==MultUpdateNode.ADD)
202 if (mun.getType()==MultUpdateNode.REMOVE)
207 cantremove.remove(gn);
209 cantremove.remove(gn2);
211 cantremove.remove(gn3);
213 if (ismodify&&((numadd==0)||(numremove==0))) {
214 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
215 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
216 GraphNode gn3=e2.getTarget();
217 TermNode tn3=(TermNode)gn3.getOwner();
218 if (tn3.getType()!=TermNode.UPDATE)
220 MultUpdateNode mun=tn3.getUpdate();
221 if (((mun.getType()==MultUpdateNode.ADD)||
222 (mun.getType()==MultUpdateNode.REMOVE))&&
223 (!mustremove.contains(gn3)))
230 if (!mustremove.contains(gn)) {
237 /* Searches scope nodes + compensation nodes */
238 for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
239 GraphNode gn=(GraphNode)it.next();
241 if (nodes.contains(gn)) {
242 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
243 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
244 GraphNode gn2=e.getTarget();
245 TermNode tn2=(TermNode)gn2.getOwner();
247 if ((tn2.getType()==TermNode.CONSEQUENCE)&&
248 !mustremove.contains(gn2))
252 if (tn2.getType()!=TermNode.UPDATE)
254 /* We have a compensation node */
255 boolean containsgn=cantremove.contains(gn);
256 boolean containsgn2=cantremove.contains(gn2);
260 Set cycle=GraphNode.findcycles(cantremove);
261 if (cycle.contains(gn2)) {
262 if (!mustremove.contains(gn2)) {
267 if (!mustremove.contains(gn2))
271 cantremove.remove(gn);
273 cantremove.remove(gn2);
277 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
278 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
279 GraphNode gn2=e.getTarget();
280 TermNode tn2=(TermNode)gn2.getOwner();
281 if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
282 !mustremove.contains(gn2)) {
283 if (!cantremove.contains(gn2)) {
292 couldremove.removeAll(mustremove);
293 couldremove.removeAll(cantremove);
295 Vector couldremovevector=new Vector();
296 couldremovevector.addAll(couldremove);
297 Vector combination=new Vector();
299 continue; //recalculate
302 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
303 } catch (Exception e) {
308 System.out.println("Searching set of "+couldremove.size()+" nodes.");
309 System.out.println("Eliminated must "+mustremove.size()+" nodes");
310 System.out.println("Eliminated cant "+cantremove.size()+" nodes");
311 System.out.println("Searching following set:");
312 for(Iterator it=couldremove.iterator();it.hasNext();) {
313 GraphNode gn=(GraphNode)it.next();
314 System.out.println(gn.getTextLabel());
316 System.out.println("Must remove set:");
317 for(Iterator it=mustremove.iterator();it.hasNext();) {
318 GraphNode gn=(GraphNode)it.next();
319 System.out.println(gn.getTextLabel());
321 System.out.println("Cant remove set:");
322 for(Iterator it=cantremove.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);
347 System.out.println("Search failed!");
352 private void checkmodify(Set removednodes) {
353 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
354 GraphNode gn=(GraphNode)it.next();
355 TermNode tn=(TermNode)gn.getOwner();
356 AbstractRepair ar=tn.getAbstract();
358 /* Has MODIFYRELATION */
359 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
362 for(Iterator it2=gn.edges();it2.hasNext();) {
363 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
364 GraphNode gn2=edge.getTarget();
365 TermNode tn2=(TermNode)gn2.getOwner();
366 if (!removednodes.contains(gn2)&&
367 tn2.getType()==TermNode.UPDATE) {
368 MultUpdateNode mun=tn2.getUpdate();
370 if (mun.getType()==MultUpdateNode.ADD)
372 if (mun.getType()==MultUpdateNode.REMOVE)
376 if ((numadd==0)||(numremove==0)) {
377 for(Iterator it2=gn.edges();it2.hasNext();) {
378 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
379 GraphNode gn2=edge.getTarget();
380 TermNode tn2=(TermNode)gn2.getOwner();
381 if (!removednodes.contains(gn2)&&
382 tn2.getType()==TermNode.UPDATE) {
383 MultUpdateNode mun=tn2.getUpdate();
384 if ((mun.getType()==MultUpdateNode.ADD)
385 ||(mun.getType()==MultUpdateNode.REMOVE)) {
386 removednodes.add(gn2);
395 private static Set buildset(Vector combination, Vector couldremove) {
397 for(int i=0;i<combination.size();i++) {
398 int index=((Integer)combination.get(i)).intValue();
399 Object o=couldremove.get(index);
408 private static boolean illegal(Vector combination, Vector couldremove) {
409 if (combination.size()>couldremove.size())
413 private static void increment(Vector combination, Vector couldremove) {
414 boolean incremented=false;
415 boolean forcereset=false;
416 for(int i=0;i<combination.size();i++) {
417 int newindex=((Integer)combination.get(i)).intValue()+1;
418 if (newindex==couldremove.size()||forcereset) {
420 if ((i+1)==combination.size()) {
423 newindex=((Integer)combination.get(i+1)).intValue()+2;
424 for(int j=i;j>=0;j--) {
425 combination.set(j,new Integer(newindex));
428 if (newindex>couldremove.size())
432 combination.set(i,new Integer(newindex));
436 if (incremented==false) /* Increase length */ {
437 combination.add(new Integer(0));
438 System.out.println("Expanding to :"+combination.size());
442 /* This function checks the graph as a whole for bad cycles */
443 public int checkAll(Collection removed) {
444 Set nodes=new HashSet();
445 nodes.addAll(termination.conjunctions);
446 nodes.removeAll(removed);
447 GraphNode.computeclosure(nodes,removed);
448 Set cycles=GraphNode.findcycles(nodes);
449 for(Iterator it=cycles.iterator();it.hasNext();) {
450 GraphNode gn=(GraphNode)it.next();
451 TermNode tn=(TermNode)gn.getOwner();
452 switch(tn.getType()) {
453 case TermNode.UPDATE:
454 case TermNode.CONJUNCTION:
456 case TermNode.ABSTRACT:
457 case TermNode.RULESCOPE:
458 case TermNode.CONSEQUENCE:
466 /* This function checks that
467 1) All abstract repairs have a corresponding data structure update
469 2) All scope nodes have either a consequence node or a compensation
470 node that isn't removed.
472 public int checkRepairs(Collection removed) {
473 Set nodes=new HashSet();
474 nodes.addAll(termination.conjunctions);
475 nodes.removeAll(removed);
476 GraphNode.computeclosure(nodes,removed);
477 Set toretain=new HashSet();
478 toretain.addAll(termination.abstractrepair);
479 toretain.addAll(termination.scopenodes);
480 nodes.retainAll(toretain);
481 /* Nodes is now the reachable set of abstractrepairs */
482 /* Check to see that each has an implementation */
483 for(Iterator it=nodes.iterator();it.hasNext();) {
484 GraphNode gn=(GraphNode)it.next();
485 TermNode tn=(TermNode)gn.getOwner();
486 if (tn.getType()==TermNode.RULESCOPE) {
487 boolean foundnode=false;
488 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
489 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
490 GraphNode gn2=edge.getTarget();
491 if (!removed.contains(gn2)) {
492 TermNode tn2=(TermNode)gn2.getOwner();
493 if ((tn2.getType()==TermNode.CONSEQUENCE)||
494 (tn2.getType()==TermNode.UPDATE)) {
501 System.out.println(gn.getTextLabel());
504 } else if (tn.getType()==TermNode.ABSTRACT) {
505 boolean foundnode=false;
506 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
507 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
508 GraphNode gn2=edge.getTarget();
509 if (!removed.contains(gn2)) {
510 TermNode tn2=(TermNode)gn2.getOwner();
511 if (tn2.getType()==TermNode.UPDATE) {
519 } else throw new Error("Unanticipated Node");
523 /* This method checks that all constraints have conjunction nodes
524 and that there are no bad cycles in the abstract portion of the graph.
526 public int checkAbstract(Collection removed) {
527 Vector constraints=termination.state.vConstraints;
528 for(int i=0;i<constraints.size();i++) {
529 Constraint c=(Constraint)constraints.get(i);
530 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
532 boolean foundrepair=false;
533 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
534 GraphNode gn=(GraphNode)it.next();
535 if (!removed.contains(gn)) {
544 Set abstractnodes=new HashSet();
545 abstractnodes.addAll(termination.conjunctions);
546 abstractnodes.removeAll(removed);
547 GraphNode.computeclosure(abstractnodes,removed);
549 Set tset=new HashSet();
550 tset.addAll(termination.conjunctions);
551 tset.addAll(termination.abstractrepair);
552 tset.addAll(termination.scopenodes);
553 tset.addAll(termination.consequencenodes);
554 abstractnodes.retainAll(tset);
555 Set cycles=GraphNode.findcycles(abstractnodes);
557 for(Iterator it=cycles.iterator();it.hasNext();) {
558 GraphNode gn=(GraphNode)it.next();
559 System.out.println("NODE: "+gn.getTextLabel());
560 TermNode tn=(TermNode)gn.getOwner();
561 switch(tn.getType()) {
562 case TermNode.CONJUNCTION:
563 case TermNode.ABSTRACT:
565 case TermNode.UPDATE:
566 throw new Error("No Update Nodes should be here");