HashSet superset=new HashSet();
superset.addAll(conjunctions);
- superset.addAll(abstractrepair);
+ //superset.addAll(abstractrepair);
//superset.addAll(updatenodes);
//superset.addAll(scopenodes);
//superset.addAll(consequencenodes);
- //GraphNode.computeclosure(superset);
+ GraphNode.computeclosure(superset,null);
try {
GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
} catch (Exception e) {
e.printStackTrace();
System.exit(-1);
}
+ for(Iterator it=updatenodes.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ TermNode tn=(TermNode)gn.getOwner();
+ MultUpdateNode mun=tn.getUpdate();
+ System.out.println(gn.getTextLabel());
+ System.out.println(mun.toString());
+ }
+ GraphAnalysis ga=new GraphAnalysis(this);
}
void generateconjunctionnodes() {
"Conj ("+i+","+j+") "+dnf.get(j).name()
,tn);
conjunctions.add(gn);
- conjunctionmap.put(c,gn);
+ if (!conjunctionmap.containsKey(c))
+ conjunctionmap.put(c,new HashSet());
+ ((Set)conjunctionmap.get(c)).add(gn);
}
}
}
}
}
}
+
+ for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
+ GraphNode gn2=(GraphNode)scopeiterator.next();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ ScopeNode sn2=tn2.getScope();
+ if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
+ GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ gn.addEdge(e);
+ }
+ }
}
}
for(int j=0;j<array.length;j++) {
AbstractRepair ar=new AbstractRepair(dp,array[j],d);
TermNode tn2=new TermNode(ar);
- GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),tn2);
+ GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
gn.addEdge(e);
abstractrepair.add(gn2);
MultUpdateNode mun=new MultUpdateNode(sn);
TermNode tn2=new TermNode(mun);
GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
- UpdateNode un=new UpdateNode();
+ UpdateNode un=new UpdateNode(r);
un.addBindings(bindings);
if (j<r.numQuantifiers()) {
/* Remove quantifier */
continue;
}
}
-
+ if (!un.checkupdates()) /* Make sure we have a good update */
+ continue;
+
mun.addUpdate(un);
GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
boolean goodflag=true;
for(int i=0;i<possiblerules.size();i++) {
Rule r=(Rule)possiblerules.get(i);
- UpdateNode un=new UpdateNode();
+ UpdateNode un=new UpdateNode(r);
/* Construct bindings */
Vector bindings=new Vector();
constructbindings(bindings, r,true);
goodflag=false;break;
}
}
+ if (!un.checkupdates()) {
+ goodflag=false;
+ break;
+ }
mun.addUpdate(un);
}
if (goodflag) {
static int addtocount=0;
void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
- System.out.println("Attempting to generate add to set");
- System.out.println(ar.getPredicate().getPredicate().name());
- System.out.println(ar.getPredicate().isNegated());
+ // System.out.println("Attempting to generate add to set");
+ //System.out.println(ar.getPredicate().getPredicate().name());
+ //System.out.println(ar.getPredicate().isNegated());
for(int i=0;i<state.vRules.size();i++) {
Rule r=(Rule) state.vRules.get(i);
/* See if this is a good rule*/
- System.out.println(r.getGuardExpr().name());
+ //System.out.println(r.getGuardExpr().name());
if ((r.getInclusion() instanceof SetInclusion&&
ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
(r.getInclusion() instanceof RelationInclusion&&
/* First solve for quantifiers */
Vector bindings=new Vector();
/* Construct bindings */
- System.out.println("Attempting to generate add to set: #2");
+ //System.out.println("Attempting to generate add to set: #2");
if (!constructbindings(bindings,r,false))
continue;
- System.out.println("Attempting to generate add to set: #3");
+ //System.out.println("Attempting to generate add to set: #3");
//Generate add instruction
DNFRule dnfrule=r.getDNFGuardExpr();
for(int j=0;j<dnfrule.size();j++) {
Inclusion inc=r.getInclusion();
- UpdateNode un=new UpdateNode();
+ UpdateNode un=new UpdateNode(r);
un.addBindings(bindings);
/* Now build update for tuple/set inclusion condition */
if(inc instanceof SetInclusion) {
//Finally build necessary updates to satisfy conjunction
RuleConjunction ruleconj=dnfrule.get(j);
/* Add in updates for quantifiers */
- System.out.println("Attempting to generate add to set #4");
+ //System.out.println("Attempting to generate add to set #4");
MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
TermNode tn=new TermNode(mun);
GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
if (processquantifers(gn2,un, r)&&debugdd()&&
- processconjunction(un,ruleconj)) {
- System.out.println("Attempting to generate add to set #5");
+ processconjunction(un,ruleconj)&&
+ un.checkupdates()) {
+ //System.out.println("Attempting to generate add to set #5");
mun.addUpdate(un);
GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
addtocount++;
}
boolean debugdd() {
- System.out.println("Attempting to generate add to set DD");
+ //System.out.println("Attempting to generate add to set DD");
return true;
}