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(cycles);
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)) {
117 System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
118 return null; // Out of luck
122 /* Search through abstract repair actions & correspond data structure updates */
123 for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) {
124 GraphNode gn=(GraphNode)it.next();
125 TermNode tn=(TermNode)gn.getOwner();
127 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
128 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
129 GraphNode gn2=e.getTarget();
130 TermNode tn2=(TermNode)gn2.getOwner();
131 if (tn2.getType()!=TermNode.UPDATE)
134 boolean containsgn=cantremove.contains(gn);
135 boolean containsgn2=cantremove.contains(gn2);
140 Set cycle=GraphNode.findcycles(cantremove);
141 if (cycle.contains(gn2)) {
142 if (!mustremove.contains(gn2)) {
148 cantremove.remove(gn);
150 cantremove.remove(gn2);
154 /* Searches individual conjunctions + abstract action +updates for cycles */
155 for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
156 GraphNode gn=(GraphNode)it.next();
157 boolean foundnocycle=false;
159 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
160 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
161 GraphNode gn2=e.getTarget();
162 TermNode tn2=(TermNode)gn2.getOwner();
163 if (tn2.getType()!=TermNode.ABSTRACT)
165 AbstractRepair ar=tn2.getAbstract();
166 boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
167 int numadd=0;int numremove=0;
169 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
170 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
171 GraphNode gn3=e2.getTarget();
172 TermNode tn3=(TermNode)gn3.getOwner();
173 if (tn3.getType()!=TermNode.UPDATE)
176 boolean containsgn=cantremove.contains(gn);
177 boolean containsgn2=cantremove.contains(gn2);
178 boolean containsgn3=cantremove.contains(gn3);
182 Set cycle=GraphNode.findcycles(cantremove);
183 if (cycle.contains(gn3)) {
184 if (!mustremove.contains(gn3)) {
189 if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
192 MultUpdateNode mun=tn3.getUpdate();
193 if (mun.getType()==MultUpdateNode.ADD)
195 if (mun.getType()==MultUpdateNode.REMOVE)
200 cantremove.remove(gn);
202 cantremove.remove(gn2);
204 cantremove.remove(gn3);
206 if (ismodify&&((numadd==0)||(numremove==0))) {
207 for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
208 GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
209 GraphNode gn3=e2.getTarget();
210 TermNode tn3=(TermNode)gn3.getOwner();
211 if (tn3.getType()!=TermNode.UPDATE)
213 MultUpdateNode mun=tn3.getUpdate();
214 if (((mun.getType()==MultUpdateNode.ADD)||
215 (mun.getType()==MultUpdateNode.REMOVE))&&
216 (!mustremove.contains(gn3)))
223 if (!mustremove.contains(gn)) {
230 /* Searches scope nodes + compensation nodes */
231 for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
232 GraphNode gn=(GraphNode)it.next();
233 boolean foundcompensation=false;
234 if (nodes.contains(gn)) {
235 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
236 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
237 GraphNode gn2=e.getTarget();
238 TermNode tn2=(TermNode)gn2.getOwner();
240 if (tn2.getType()!=TermNode.UPDATE)
242 /* We have a compensation node */
243 boolean containsgn=cantremove.contains(gn);
244 boolean containsgn2=cantremove.contains(gn2);
248 Set cycle=GraphNode.findcycles(cantremove);
249 if (cycle.contains(gn2)) {
250 if (!mustremove.contains(gn2)) {
255 if (!mustremove.contains(gn2))
256 foundcompensation=true;
259 cantremove.remove(gn);
261 cantremove.remove(gn2);
264 if (!foundcompensation) {
265 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
266 GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
267 GraphNode gn2=e.getTarget();
268 TermNode tn2=(TermNode)gn2.getOwner();
269 if (tn2.getType()==TermNode.UPDATE) {
276 couldremove.removeAll(mustremove);
277 couldremove.removeAll(cantremove);
279 Vector couldremovevector=new Vector();
280 couldremovevector.addAll(couldremove);
281 Vector combination=new Vector();
283 continue; //recalculate
286 GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes);
287 } catch (Exception e) {
292 System.out.println("Searching set of "+couldremove.size()+" nodes.");
293 System.out.println("Eliminated must "+mustremove.size()+" nodes");
294 System.out.println("Eliminated cant "+cantremove.size()+" nodes");
295 System.out.println("Searching following set:");
296 for(Iterator it=couldremove.iterator();it.hasNext();) {
297 GraphNode gn=(GraphNode)it.next();
298 System.out.println(gn.getTextLabel());
303 if (illegal(combination,couldremovevector))
305 Set combinationset=buildset(combination,couldremovevector);
306 checkmodify(combinationset);
307 combinationset.addAll(mustremove);
308 if (combinationset!=null) {
309 System.out.println("Checkabstract="+checkAbstract(combinationset));
310 System.out.println("Checkrepairs="+checkRepairs(combinationset));
311 System.out.println("Checkall="+checkAll(combinationset));
313 if (checkAbstract(combinationset)==0&&
314 checkRepairs(combinationset)==0&&
315 checkAll(combinationset)==0) {
316 return combinationset;
319 increment(combination,couldremovevector);
321 System.out.println("Search failed!");
326 private void checkmodify(Set removednodes) {
327 for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) {
328 GraphNode gn=(GraphNode)it.next();
329 TermNode tn=(TermNode)gn.getOwner();
330 AbstractRepair ar=tn.getAbstract();
332 /* Has MODIFYRELATION */
333 if (ar.getType()==AbstractRepair.MODIFYRELATION) {
336 for(Iterator it2=gn.edges();it2.hasNext();) {
337 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
338 GraphNode gn2=edge.getTarget();
339 TermNode tn2=(TermNode)gn2.getOwner();
340 if (!removednodes.contains(gn2)&&
341 tn2.getType()==TermNode.UPDATE) {
342 MultUpdateNode mun=tn2.getUpdate();
344 if (mun.getType()==MultUpdateNode.ADD)
346 if (mun.getType()==MultUpdateNode.REMOVE)
350 if ((numadd==0)||(numremove==0)) {
351 for(Iterator it2=gn.edges();it2.hasNext();) {
352 GraphNode.Edge edge=(GraphNode.Edge)it2.next();
353 GraphNode gn2=edge.getTarget();
354 TermNode tn2=(TermNode)gn2.getOwner();
355 if (!removednodes.contains(gn2)&&
356 tn2.getType()==TermNode.UPDATE) {
357 MultUpdateNode mun=tn2.getUpdate();
358 if ((mun.getType()==MultUpdateNode.ADD)
359 ||(mun.getType()==MultUpdateNode.REMOVE)) {
360 removednodes.add(gn2);
369 private static Set buildset(Vector combination, Vector couldremove) {
371 for(int i=0;i<combination.size();i++) {
372 int index=((Integer)combination.get(i)).intValue();
373 Object o=couldremove.get(index);
382 private static boolean illegal(Vector combination, Vector couldremove) {
383 if (combination.size()>couldremove.size())
387 private static void increment(Vector combination, Vector couldremove) {
388 boolean incremented=false;
389 boolean forcereset=false;
390 for(int i=0;i<combination.size();i++) {
391 int newindex=((Integer)combination.get(i)).intValue()+1;
392 if (newindex==couldremove.size()||forcereset) {
394 if ((i+1)==combination.size()) {
397 newindex=((Integer)combination.get(i+1)).intValue()+2;
398 for(int j=i;j>=0;j--) {
399 combination.set(j,new Integer(newindex));
402 if (newindex>couldremove.size())
406 combination.set(i,new Integer(newindex));
410 if (incremented==false) /* Increase length */ {
411 combination.add(new Integer(0));
412 System.out.println("Expanding to :"+combination.size());
416 /* This function checks the graph as a whole for bad cycles */
417 public int checkAll(Collection removed) {
418 Set nodes=new HashSet();
419 nodes.addAll(termination.conjunctions);
420 nodes.removeAll(removed);
421 GraphNode.computeclosure(nodes,removed);
422 Set cycles=GraphNode.findcycles(nodes);
423 for(Iterator it=cycles.iterator();it.hasNext();) {
424 GraphNode gn=(GraphNode)it.next();
425 TermNode tn=(TermNode)gn.getOwner();
426 switch(tn.getType()) {
427 case TermNode.UPDATE:
428 case TermNode.CONJUNCTION:
430 case TermNode.ABSTRACT:
431 case TermNode.RULESCOPE:
432 case TermNode.CONSEQUENCE:
440 /* This function checks that
441 1) All abstract repairs have a corresponding data structure update
443 2) All scope nodes have either a consequence node or a compensation
444 node that isn't removed.
446 public int checkRepairs(Collection removed) {
447 Set nodes=new HashSet();
448 nodes.addAll(termination.conjunctions);
449 nodes.removeAll(removed);
450 GraphNode.computeclosure(nodes,removed);
451 Set toretain=new HashSet();
452 toretain.addAll(termination.abstractrepair);
453 toretain.addAll(termination.scopenodes);
454 nodes.retainAll(toretain);
455 /* Nodes is now the reachable set of abstractrepairs */
456 /* Check to see that each has an implementation */
457 for(Iterator it=nodes.iterator();it.hasNext();) {
458 GraphNode gn=(GraphNode)it.next();
459 TermNode tn=(TermNode)gn.getOwner();
460 if (tn.getType()==TermNode.RULESCOPE) {
461 boolean foundnode=false;
462 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
463 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
464 GraphNode gn2=edge.getTarget();
465 if (!removed.contains(gn2)) {
466 TermNode tn2=(TermNode)gn2.getOwner();
467 if ((tn2.getType()==TermNode.CONSEQUENCE)||
468 (tn2.getType()==TermNode.UPDATE)) {
475 System.out.println(gn.getTextLabel());
478 } else if (tn.getType()==TermNode.ABSTRACT) {
479 boolean foundnode=false;
480 for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
481 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
482 GraphNode gn2=edge.getTarget();
483 if (!removed.contains(gn2)) {
484 TermNode tn2=(TermNode)gn2.getOwner();
485 if (tn2.getType()==TermNode.UPDATE) {
493 } else throw new Error("Unanticipated Node");
497 /* This method checks that all constraints have conjunction nodes
498 and that there are no bad cycles in the abstract portion of the graph.
500 public int checkAbstract(Collection removed) {
501 Vector constraints=termination.state.vConstraints;
502 for(int i=0;i<constraints.size();i++) {
503 Constraint c=(Constraint)constraints.get(i);
504 Set conjunctionset=(Set)termination.conjunctionmap.get(c);
506 boolean foundrepair=false;
507 for(Iterator it=conjunctionset.iterator();it.hasNext();) {
508 GraphNode gn=(GraphNode)it.next();
509 if (!removed.contains(gn)) {
518 Set abstractnodes=new HashSet();
519 abstractnodes.addAll(termination.conjunctions);
520 abstractnodes.removeAll(removed);
521 GraphNode.computeclosure(abstractnodes,removed);
523 Set tset=new HashSet();
524 tset.addAll(termination.conjunctions);
525 tset.addAll(termination.abstractrepair);
526 tset.addAll(termination.scopenodes);
527 tset.addAll(termination.consequencenodes);
528 abstractnodes.retainAll(tset);
529 Set cycles=GraphNode.findcycles(abstractnodes);
531 for(Iterator it=cycles.iterator();it.hasNext();) {
532 GraphNode gn=(GraphNode)it.next();
533 System.out.println("NODE: "+gn.getTextLabel());
534 TermNode tn=(TermNode)gn.getOwner();
535 switch(tn.getType()) {
536 case TermNode.CONJUNCTION:
537 case TermNode.ABSTRACT:
539 case TermNode.UPDATE:
540 throw new Error("No Update Nodes should be here");