5 class ModelRuleDependence {
8 HashMap ruletonode, nodetorule;
9 // Stores references to negated edges
14 private final int NODEPENDENCY=0;
15 private final int NORMDEPENDENCY=1;
16 private final int NEGDEPENDENCY=2;
18 private ModelRuleDependence(State state) {
20 this.nodes=new HashSet();
21 this.ruletonode=new HashMap();
22 this.nodetorule=new HashMap();
23 this.negatededges=new HashSet();
24 this.sccCache=new HashMap();
27 public static ModelRuleDependence doAnalysis(State state) {
28 ModelRuleDependence mrd=new ModelRuleDependence(state);
31 mrd.scc=GraphNode.DFS.computeSCC(mrd.nodes);
32 if (mrd.checkForNegatedDependences())
33 throw new Error("Negated Dependence");
41 /** Gives strongly connected components in reverse topological
43 public Set getSCC(int i) {
44 Integer in=new Integer(i);
45 if (sccCache.containsKey(in))
46 return (Set) sccCache.get(in);
47 Set nodescc=scc.getSCC(i);
48 HashSet rulescc=new HashSet();
49 for (Iterator nodeit=nodescc.iterator();nodeit.hasNext();) {
50 GraphNode gn=(GraphNode) nodeit.next();
51 Rule r=(Rule)nodetorule.get(gn);
54 sccCache.put(in,rulescc);
58 public boolean hasCycle(Rule r) {
59 return hasCycle(getComponent(r));
62 public boolean hasCycle(int i) {
63 return scc.hasCycle(i);
66 public int getComponent(Rule r) {
67 return scc.getComponent((GraphNode)ruletonode.get(r));
70 /** Returns true if there are any negated dependence cycles, false
72 private boolean checkForNegatedDependences() {
73 for(Iterator it=negatededges.iterator();it.hasNext();) {
74 GraphNode.Edge e=(GraphNode.Edge)it.next();
75 int scc1=scc.getComponent(e.getSource());
76 int scc2=scc.getComponent(e.getTarget());
83 /** Build mapping between nodes and rules */
84 private void generateNodes() {
85 for(int i=0;i<state.vRules.size();i++) {
86 GraphNode gn=new GraphNode("Rule"+i);
87 ruletonode.put(state.vRules.get(i),gn);
88 nodetorule.put(gn,state.vRules.get(i));
93 /** Generate edges between rule nodes */
94 private void generateEdges() {
95 for(int i=0;i<state.vRules.size();i++) {
96 for(int j=0;j<state.vRules.size();j++) {
97 Rule r1=(Rule)state.vRules.get(i);
98 Rule r2=(Rule)state.vRules.get(j);
104 private void generateEdge(Rule r1,Rule r2) {
105 Descriptor d=(Descriptor) r1.getInclusion().getTargetDescriptors().iterator().next();
106 int dep=checkBody(d,r2.getDNFGuardExpr());
107 if (dep==NODEPENDENCY)
108 dep=checkQuantifiers(d,r2);
109 if (dep==NODEPENDENCY)
111 GraphNode gn1=(GraphNode) ruletonode.get(r1);
112 GraphNode gn2=(GraphNode) ruletonode.get(r2);
113 GraphNode.Edge edge=new GraphNode.Edge("dependency",gn2);
115 if (dep==NEGDEPENDENCY)
116 negatededges.add(edge);
119 private int checkBody(Descriptor d, DNFRule drule) {
120 boolean dependency=false;
121 for(int i=0;i<drule.size();i++) {
122 RuleConjunction rconj=drule.get(i);
123 for(int j=0;j<rconj.size();j++){
124 DNFExpr dexpr=rconj.get(j);
125 Expr e=dexpr.getExpr();
126 if (e.usesDescriptor(d)) {
127 boolean negated=dexpr.getNegation();
129 return NEGDEPENDENCY;
136 return NORMDEPENDENCY;
141 private int checkQuantifiers(Descriptor d, Quantifiers qs) {
142 for (int i=0;i<qs.numQuantifiers();i++) {
143 Quantifier q=qs.getQuantifier(i);
144 if (q.getRequiredDescriptors().contains(d))
145 return NORMDEPENDENCY;