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 SetDescriptor bsd=null;
109 if (d instanceof SetDescriptor) {
110 SetInclusion si=(SetInclusion)r1.getInclusion();
111 if (si.getExpr() instanceof VarExpr) {
112 VarDescriptor vd=((VarExpr)si.getExpr()).getVar();
116 dep=checkQuantifiers(bsd,d,r2);
118 if (dep==NODEPENDENCY)
120 GraphNode gn1=(GraphNode) ruletonode.get(r1);
121 GraphNode gn2=(GraphNode) ruletonode.get(r2);
122 GraphNode.Edge edge=new GraphNode.Edge("dependency",gn2);
124 if (dep==NEGDEPENDENCY)
125 negatededges.add(edge);
128 private int checkBody(Descriptor d, DNFRule drule) {
129 boolean dependency=false;
130 for(int i=0;i<drule.size();i++) {
131 RuleConjunction rconj=drule.get(i);
132 for(int j=0;j<rconj.size();j++) {
133 DNFExpr dexpr=rconj.get(j);
134 Expr e=dexpr.getExpr();
135 Set descset=e.getRequiredDescriptors();
136 descset=SetDescriptor.expand(descset);
137 if (descset.contains(d)) {
138 boolean negated=dexpr.getNegation();
140 return NEGDEPENDENCY;
147 return NORMDEPENDENCY;
152 private int checkQuantifiers(SetDescriptor bsd, Descriptor d, Quantifiers qs) {
153 for (int i=0;i<qs.numQuantifiers();i++) {
154 Quantifier q=qs.getQuantifier(i);
155 if (q instanceof SetQuantifier&&
156 d instanceof SetDescriptor) {
157 SetQuantifier sq=(SetQuantifier)q;
158 SetDescriptor sd=(SetDescriptor)d;
159 if (sq.getSet().isSubset(sd)&&
160 ((bsd==null)||!bsd.isSubset(sq.getSet())))
161 return NORMDEPENDENCY;
162 } else if (q.getRequiredDescriptors().contains(d))
163 return NORMDEPENDENCY;