package MCC.IR;
+import java.util.*;
class AbstractInterferes {
static public boolean interferes(AbstractRepair ar, Rule r, boolean satisfy) {
return true;
}
+ static public boolean interferes(ScopeNode sn, DNFPredicate dp) {
+ if (!sn.getSatisfy()&&(sn.getDescriptor() instanceof SetDescriptor)) {
+ Rule r=sn.getRule();
+ Set target=r.getInclusion().getTargetDescriptors();
+ boolean match=false;
+ for(int i=0;i<r.numQuantifiers();i++) {
+ Quantifier q=r.getQuantifier(i);
+ if (q instanceof SetQuantifier) {
+ SetQuantifier sq=(SetQuantifier) q;
+ if (target.contains(sq.getSet())) {
+ match=true;
+ break;
+ }
+ }
+ }
+ if (match&&
+ sn.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+ boolean neg=dp.isNegated();
+ Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
+ int size=((ExprPredicate)dp.getPredicate()).leftsize();
+ if (neg) {
+ /* remove negation through opcode translation */
+ if (op==Opcode.GT)
+ op=Opcode.LE;
+ else if (op==Opcode.GE)
+ op=Opcode.LT;
+ else if (op==Opcode.EQ)
+ op=Opcode.NE;
+ else if (op==Opcode.NE)
+ op=Opcode.EQ;
+ else if (op==Opcode.LT)
+ op=Opcode.GE;
+ else if (op==Opcode.LE)
+ op=Opcode.GT;
+ }
+ if ((op==Opcode.GE)&&
+ ((size==0)||(size==1)))
+ return false;
+ if ((op==Opcode.GT)&&
+ (size==0))
+ return false;
+ }
+ }
+ return interferes(sn.getDescriptor(), sn.getSatisfy(),dp);
+ }
+
static public boolean interferes(Descriptor des, boolean satisfy, DNFPredicate dp) {
if ((des!=dp.getPredicate().getDescriptor()) &&
((des instanceof SetDescriptor)||
return expr.freeVars();
}
+ public void findmatch(Descriptor d, Set s) {
+ expr.findmatch(d,s);
+ }
+
public CastExpr(TypeDescriptor type, Expr expr) {
this.type = type;
this.expr = expr;
import java.util.*;
class ConcreteInterferes {
+
+ static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
+ Descriptor updated_des=update.getDescriptor();
+ Inclusion inclusion=r.getInclusion();
+ if (inclusion instanceof RelationInclusion) {
+ RelationInclusion ri=(RelationInclusion)inclusion;
+ if (ri.getLeftExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getLeftExpr()))
+ return true;
+ if (ri.getRightExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,ri.getRightExpr()))
+ return true;
+ } else if (inclusion instanceof SetInclusion) {
+ SetInclusion si=(SetInclusion)inclusion;
+ if (si.getExpr().usesDescriptor(updated_des)&&interferesinclusion(un,update,r,si.getExpr()))
+ return true;
+ } else throw new Error();
+ return false;
+ }
+
+ static public boolean interferesinclusion(UpdateNode un, Updates update, Rule r, Expr inclusionexpr) {
+ Descriptor updated_des=update.getDescriptor();
+ if (updated_des instanceof FieldDescriptor) {
+ /* Build variable correspondance */
+ HashSet set=new HashSet();
+ inclusionexpr.findmatch(updated_des,set);
+
+ for(Iterator matchit=set.iterator();matchit.hasNext();) {
+ DotExpr dotexpr=(DotExpr)matchit.next();
+ DotExpr updateexpr=(DotExpr)update.getLeftExpr();
+ while(true) {
+ if (dotexpr.getField()!=updateexpr.getField())
+ return true;
+ Expr de=dotexpr.getExpr();
+ Expr ue=updateexpr.getExpr();
+ if ((de instanceof DotExpr)&&(ue instanceof DotExpr)) {
+ dotexpr=(DotExpr)de;
+ updateexpr=(DotExpr)ue;
+ } else if ((de instanceof VarExpr)&&(ue instanceof VarExpr)) {
+ VarDescriptor dvd=((VarExpr)de).getVar();
+ VarDescriptor uvd=((VarExpr)ue).getVar();
+ if (interferesinclusion(un,r,dvd,uvd))
+ return true;
+ else
+ break;
+ } else
+ return true;
+ }
+ }
+ } else if (updated_des instanceof VarDescriptor) {
+ /* We have a VarDescriptor - no correspondance necessary */
+ VarDescriptor vd=(VarDescriptor)updated_des;
+ if (interferesinclusion(un,r,vd,vd))
+ return true;
+ } else throw new Error();
+ return false;
+ }
+
+ static public boolean interferesinclusion(UpdateNode un, Rule r, VarDescriptor dvd, VarDescriptor uvd) {
+ DNFRule negrule=r.getDNFNegGuardExpr();
+ HashMap remap=new HashMap();
+ remap.put(dvd,uvd);
+
+ for(int i=0;i<negrule.size();i++) {
+ RuleConjunction rconj=negrule.get(i);
+ boolean good=true;
+ for(int j=0;j<rconj.size();j++) {
+ DNFExpr dexpr=rconj.get(j);
+ if (dexpr.getExpr() instanceof OpExpr) {
+ OpExpr expr=(OpExpr)dexpr.getExpr();
+ Expr lexpr=expr.getLeftExpr();
+ Expr rexpr=expr.getRightExpr();
+
+ boolean varok=true;
+ Set vars=rexpr.freeVars();
+ if (vars!=null)
+ for(Iterator it=vars.iterator();it.hasNext();) {
+ VarDescriptor vd=(VarDescriptor) it.next();
+ if (!vd.isGlobal()) {
+ /* VarDescriptor isn't a global */
+ if (dvd!=vd) {
+ varok=false;
+ break;
+ }
+ }
+ }
+
+ if (!varok)
+ continue;
+
+
+
+ Opcode op=expr.getOpcode();
+
+ if (dexpr.getNegation()) {
+ /* remove negation through opcode translation */
+ if (op==Opcode.GT)
+ op=Opcode.LE;
+ else if (op==Opcode.GE)
+ op=Opcode.LT;
+ else if (op==Opcode.EQ)
+ op=Opcode.NE;
+ else if (op==Opcode.NE)
+ op=Opcode.EQ;
+ else if (op==Opcode.LT)
+ op=Opcode.GE;
+ else if (op==Opcode.LE)
+ op=Opcode.GT;
+ }
+ boolean match=false;
+ for(int k=0;k<un.numUpdates();k++) {
+ Updates update=un.getUpdate(k);
+ if(update.isExpr()) {
+ Set uvars=update.getRightExpr().freeVars();
+ boolean freevarok=true;
+ if (uvars!=null)
+ for(Iterator it=uvars.iterator();it.hasNext();) {
+ VarDescriptor vd=(VarDescriptor) it.next();
+ if (!vd.isGlobal()) {
+ /* VarDescriptor isn't a global */
+ if (uvd!=vd) {
+ freevarok=false;
+ break;
+ }
+ }
+ }
+ if (!freevarok)
+ continue;
+
+ Opcode op2=update.getOpcode();
+ if ((op2==op)||
+ ((op2==Opcode.GT)&&(op==Opcode.GE))||
+ ((op2==Opcode.LT)&&(op==Opcode.LE))||
+ ((op2==Opcode.EQ)&&((op==Opcode.GE)||(op==Opcode.LE)))) {
+ /* Operations match*/
+ if (lexpr.equals(remap,update.getLeftExpr())&&
+ rexpr.equals(remap,update.getRightExpr())) {
+ match=true;
+ break;
+ }
+ }
+ }
+ }
+ if (!match) {
+ good=false;
+ break;
+ }
+ } else {
+ /* TODO: Check to see if there is an abstract repair */
+ good=false;
+ break; /* try next conjunction */
+ }
+ }
+ if (good)
+ return false;
+ }
+ return true;
+ }
+
static public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
if (!initialinterferes(mun,r,satisfy)) /* Can't falsify a rule adding something to a set on an initial addition*/
return false;
continue;
- if (r.getInclusion().usesDescriptor(updated_des))
- return true; /* Interferes with inclusion condition */
+ if (r.getInclusion().usesDescriptor(updated_des)) {
+ if (satisfy) {
+ if (interferesinclusion(un, update, r))
+ return true;
+ } else
+ return true; /* Interferes with inclusion condition */
+ }
for(int k=0;k<drule.size();k++) {
RuleConjunction rconj=drule.get(k);
Expr lexpr1=update.getLeftExpr();
Expr rexpr1=update.getRightExpr();
boolean good=true;
- for(Iterator it=vars.iterator();it.hasNext();) {
- VarDescriptor vd=(VarDescriptor) it.next();
- if (un.getBinding(vd)!=null) {
- /* VarDescriptor isn't a global */
- if (update.getVar()!=vd) {
- good=false;
- break;
+ if (vars!=null)
+ for(Iterator it=vars.iterator();it.hasNext();) {
+ VarDescriptor vd=(VarDescriptor) it.next();
+ if (!vd.isGlobal()) {
+ /* VarDescriptor isn't a global */
+ if (update.getVar()!=vd) {
+ good=false;
+ break;
+ }
}
}
- }
if (good&&(dexpr.getExpr() instanceof OpExpr)) {
OpExpr expr=(OpExpr)dexpr.getExpr();
Expr lexpr2=expr.getLeftExpr();
leftdescriptor=((VarExpr)e).getVar();
} else throw new Error("Bad Expr");
- for(Iterator it=vars.iterator();it.hasNext();) {
- VarDescriptor vd=(VarDescriptor) it.next();
- if (un.getBinding(vd)!=null) {
- /* VarDescriptor isn't a global */
- if (leftdescriptor!=vd) {
- good=false;
- break;
+ if (vars!=null)
+ for(Iterator it=vars.iterator();it.hasNext();) {
+ VarDescriptor vd=(VarDescriptor) it.next();
+ if (!vd.isGlobal()) {
+ /* VarDescriptor isn't a global */
+ if (leftdescriptor!=vd) {
+ good=false;
+ break;
+ }
}
}
- }
if (good) {
HashMap remap=new HashMap();
remap.put(update.getVar(),leftdescriptor);
static boolean DOTYPECHECKS=false;
static boolean DONULL=false;
+ public void findmatch(Descriptor d, Set s) {
+ if (d==fd)
+ s.add(this);
+ left.findmatch(d,s);
+ if (index!=null)
+ index.findmatch(d,s);
+ }
+
public Set freeVars() {
Set lset=left.freeVars();
Set iset=null;
public Set freeVars() {
return null;
}
+
+ public void findmatch(Descriptor d, Set s) {
+ }
}
}
public Set doAnalysis() {
- HashSet nodes=new HashSet();
- nodes.addAll(termination.conjunctions);
- GraphNode.computeclosure(nodes,null);
- Set cycles=GraphNode.findcycles(nodes);
- Set couldremove=new HashSet();
- couldremove.addAll(termination.conjunctions);
- couldremove.addAll(termination.updatenodes);
- couldremove.addAll(termination.consequencenodes);
- couldremove.retainAll(cycles);
- Vector constraints=termination.state.vConstraints;
- for(int i=0;i<constraints.size();i++) {
- Constraint c=(Constraint)constraints.get(i);
- Set conjunctionset=(Set)termination.conjunctionmap.get(c);
- if (conjunctionset.size()==1)
- couldremove.removeAll(conjunctionset);
- }
+ HashSet cantremove=new HashSet();
+ HashSet mustremove=new HashSet();
+ cantremove.addAll(termination.scopenodes);
+ cantremove.addAll(termination.abstractrepair);
+ while(true) {
+ boolean change=false;
+ HashSet nodes=new HashSet();
+ nodes.addAll(termination.conjunctions);
+ nodes.removeAll(mustremove);
+ GraphNode.computeclosure(nodes,mustremove);
+ Set cycles=GraphNode.findcycles(nodes);
+ Set couldremove=new HashSet();
+ couldremove.addAll(termination.conjunctions);
+ couldremove.addAll(termination.updatenodes);
+ couldremove.addAll(termination.consequencenodes);
+ couldremove.retainAll(cycles);
- Vector couldremovevector=new Vector();
- couldremovevector.addAll(couldremove);
- Vector combination=new Vector();
- while(true) {
- if (illegal(combination,couldremovevector))
- break;
- Set combinationset=buildset(combination,couldremovevector);
- if (combinationset!=null) {
- System.out.println("Checkabstract="+checkAbstract(combinationset));
- System.out.println("Checkrepairs="+checkRepairs(combinationset));
- System.out.println("Checkall="+checkAll(combinationset));
-
- if (checkAbstract(combinationset)==0&&
- checkRepairs(combinationset)==0&&
- checkAll(combinationset)==0) {
- return combinationset;
+ /* Look for constraints which can only be satisfied one way */
+
+ Vector constraints=termination.state.vConstraints;
+ for(int i=0;i<constraints.size();i++) {
+ Constraint c=(Constraint)constraints.get(i);
+ Set conjunctionset=(Set)termination.conjunctionmap.get(c);
+ HashSet tmpset=new HashSet();
+ tmpset.addAll(conjunctionset);
+ tmpset.removeAll(mustremove);
+ if (tmpset.size()==1) {
+ int oldsize=cantremove.size();
+ cantremove.addAll(tmpset);
+ if (cantremove.size()!=oldsize)
+ change=true;
}
}
- increment(combination,couldremovevector);
+ HashSet newset=new HashSet();
+ for(Iterator cit=cantremove.iterator();cit.hasNext();) {
+ GraphNode gn=(GraphNode)cit.next();
+ boolean nomodify=true;
+ HashSet toremove=new HashSet();
+ if (termination.conjunctions.contains(gn)) {
+ for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ GraphNode gn2=e.getTarget();
+ TermNode tn2=(TermNode)gn2.getOwner();
+ if (tn2.getType()==TermNode.ABSTRACT) {
+ AbstractRepair ar=tn2.getAbstract();
+ if (ar.getType()==AbstractRepair.MODIFYRELATION) {
+ nomodify=false;
+ break;
+ }
+ HashSet updateset=new HashSet();
+ for(Iterator upit=gn2.edges();upit.hasNext();) {
+ GraphNode.Edge e2=(GraphNode.Edge)upit.next();
+ GraphNode gn3=e2.getTarget();
+ TermNode tn3=(TermNode)gn3.getOwner();
+ if (tn3.getType()==TermNode.UPDATE)
+ updateset.add(gn3);
+ }
+ updateset.removeAll(mustremove);
+ if (updateset.size()==1)
+ toremove.addAll(updateset);
+ }
+ }
+ if (nomodify) {
+ newset.addAll(toremove);
+ }
+ }
+ }
+ {
+ int oldsize=cantremove.size();
+ cantremove.addAll(newset);
+ if (cantremove.size()!=oldsize)
+ change=true;
+ }
+
+ /* Look for required actions for scope nodes */
+ for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
+ GraphNode gn=(GraphNode)scopeit.next();
+ HashSet tmpset=new HashSet();
+ for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
+ tmpset.add(e.getTarget());
+ }
+ tmpset.removeAll(mustremove);
+ if (tmpset.size()==1) {
+ int oldsize=cantremove.size();
+ cantremove.addAll(tmpset);
+ if (cantremove.size()!=oldsize)
+ change=true;
+ }
+ }
+
+ Set cycles2=GraphNode.findcycles(cantremove);
+ for(Iterator it=cycles2.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ if (termination.conjunctions.contains(gn))
+ return null; // Out of luck
+ }
+
+
+ for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ if (!cantremove.contains(gn)) {
+ cantremove.add(gn);
+ Set cycle=GraphNode.findcycles(cantremove);
+ if (cycle.contains(gn)) {
+ if (!mustremove.contains(gn)) {
+ change=true;
+ mustremove.add(gn);
+ }
+ }
+ cantremove.remove(gn);
+ }
+ }
+ couldremove.removeAll(mustremove);
+ couldremove.removeAll(cantremove);
+
+ Vector couldremovevector=new Vector();
+ couldremovevector.addAll(couldremove);
+ Vector combination=new Vector();
+ if(change)
+ continue; //recalculate
+
+ System.out.println("Searching set of "+couldremove.size()+" nodes.");
+ System.out.println("Eliminated "+mustremove.size()+" nodes");
+ System.out.println("Searching following set:");
+ for(Iterator it=couldremove.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ System.out.println(gn.getTextLabel());
+ }
+
+
+ while(true) {
+ if (illegal(combination,couldremovevector))
+ break;
+ Set combinationset=buildset(combination,couldremovevector);
+ combinationset.addAll(mustremove);
+ if (combinationset!=null) {
+ System.out.println("Checkabstract="+checkAbstract(combinationset));
+ System.out.println("Checkrepairs="+checkRepairs(combinationset));
+ System.out.println("Checkall="+checkAll(combinationset));
+
+ if (checkAbstract(combinationset)==0&&
+ checkRepairs(combinationset)==0&&
+ checkAll(combinationset)==0) {
+ return combinationset;
+ }
+ }
+ increment(combination,couldremovevector);
+ }
+ return null;
}
- return null;
}
private static Set buildset(Vector combination, Vector couldremove) {
}
private static void increment(Vector combination, Vector couldremove) {
boolean incremented=false;
+ boolean forcereset=false;
for(int i=0;i<combination.size();i++) {
int newindex=((Integer)combination.get(i)).intValue()+1;
- while(combination.contains(new Integer(newindex)))
- newindex++;
- if (newindex==couldremove.size()) {
- newindex=0;
- combination.set(i,new Integer(newindex));
+ if (newindex==couldremove.size()||forcereset) {
+ forcereset=false;
+ if ((i+1)==combination.size()) {
+ newindex=1;
+ } else
+ newindex=((Integer)combination.get(i+1)).intValue()+2;
+ for(int j=i;j>=0;j--) {
+ combination.set(j,new Integer(newindex));
+ newindex++;
+ }
+ if (newindex>couldremove.size())
+ forcereset=true;
} else {
incremented=true;
combination.set(i,new Integer(newindex));
break;
}
}
- if (incremented==false) /* Increase length */
+ if (incremented==false) /* Increase length */ {
combination.add(new Integer(0));
+ System.out.println("Expanding to :"+combination.size());
+ }
}
/* This function checks the graph as a whole for bad cycles */
Expr right;
Opcode opcode;
+ public void findmatch(Descriptor d, Set s) {
+ left.findmatch(d,s);
+ if (right!=null)
+ right.findmatch(d,s);
+ }
+
public static boolean isInt(Expr e) {
if ((e instanceof IntegerLiteralExpr)||
((e instanceof OpExpr)&&(((OpExpr)e).getLeftExpr() instanceof IntegerLiteralExpr)))
if (left instanceof RelationExpr)
return new int[] {AbstractRepair.MODIFYRELATION};
if (left instanceof SizeofExpr) {
+ Opcode op=opcode;
+ if (negated) {
+ /* remove negation through opcode translation */
+ if (op==Opcode.GT)
+ op=Opcode.LE;
+ else if (op==Opcode.GE)
+ op=Opcode.LT;
+ else if (op==Opcode.EQ)
+ op=Opcode.NE;
+ else if (op==Opcode.NE)
+ op=Opcode.EQ;
+ else if (op==Opcode.LT)
+ op=Opcode.GE;
+ else if (op==Opcode.LE)
+ op=Opcode.GT;
+ }
+
+
+
boolean isRelation=((SizeofExpr)left).setexpr instanceof ImageSetExpr;
if (isRelation) {
- if (opcode==Opcode.EQ)
+ if (op==Opcode.EQ) {
if (((IntegerLiteralExpr)right).getValue()==0)
return new int[] {AbstractRepair.REMOVEFROMRELATION};
else
return new int[] {AbstractRepair.ADDTORELATION,
- AbstractRepair.REMOVEFROMRELATION};
- if (((opcode==Opcode.GE)&&!negated)||
- ((opcode==Opcode.LE)&&negated)) {
- if (((IntegerLiteralExpr)right).getValue()==0)
- return new int[0];
- else
- return new int[]{AbstractRepair.ADDTORELATION}; }
- else
+ AbstractRepair.REMOVEFROMRELATION};
+ } else if (op==Opcode.GE||op==Opcode.GT) {
+ return new int[]{AbstractRepair.ADDTORELATION};
+ } else if (op==Opcode.LE||op==Opcode.LT) {
return new int[]{AbstractRepair.REMOVEFROMRELATION};
+ } else if (op==Opcode.NE) {
+ return new int[]{AbstractRepair.ADDTORELATION};
+ } else throw new Error();
} else {
- if (opcode==Opcode.EQ)
+ if (op==Opcode.EQ) {
if (((IntegerLiteralExpr)right).getValue()==0)
return new int[] {AbstractRepair.REMOVEFROMSET};
else
return new int[] {AbstractRepair.ADDTOSET,
AbstractRepair.REMOVEFROMSET};
-
- if (((opcode==Opcode.GE)&&!negated)||
- ((opcode==Opcode.LE)&&negated)) {
- if (((IntegerLiteralExpr)right).getValue()==0)
- return new int[0];
- else
- return new int[] {AbstractRepair.ADDTOSET}; }
- else
+ } else if (op==Opcode.GE||op==Opcode.GT) {
+ return new int[] {AbstractRepair.ADDTOSET};
+ } else if (op==Opcode.LE||op==Opcode.LT) {
return new int[] {AbstractRepair.REMOVEFROMSET};
+ } else if (op==Opcode.NE) {
+ return new int[] {AbstractRepair.ADDTOSET};
+ } else throw new Error();
}
}
throw new Error("BAD");
craux.outputline(methodcall);
craux.startblock();
craux.outputline("int maybe=0;");
- final SymbolTable st2 = un.getRule().getSymbolTable();
+ final SymbolTable st2 = un.getRule().getSymbolTable();
CodeWriter cr2 = new StandardCodeWriter(outputaux) {
public SymbolTable getSymbolTable() { return st2; }
};
generateremove=true;
} else if (opcode==Opcode.EQ) {
cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
- generateadd=true;
+ if (size==0)
+ generateadd=false;
+ else
+ generateadd=true;
generateremove=true;
} else if (opcode==Opcode.NE) {
cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
Rule r=(Rule)state.vRules.get(i);
if (r.getInclusion().getTargetDescriptors().contains(d)) {
for(int j=0;j<munremove.numUpdates();j++) {
- UpdateNode un=munremove.getUpdate(i);
+ UpdateNode un=munremove.getUpdate(j);
if (un.getRule()==r) {
/* Update for rule rule r */
String name=(String)updatenames.get(un);
cr.startblock();
VarDescriptor newobject=VarDescriptor.makeNew("newobject");
if (d instanceof RelationDescriptor) {
- VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)ep.expr).setexpr).vd;
+ VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
RelationDescriptor rd=(RelationDescriptor)d;
if (sources.relsetSource(rd,!ep.inverted())) {
/* Set Source */
HashSet superset=new HashSet();
superset.addAll(conjunctions);
+ HashSet closureset=new HashSet();
+ // closureset.addAll(updatenodes);
//superset.addAll(abstractrepair);
//superset.addAll(updatenodes);
//superset.addAll(scopenodes);
//superset.addAll(consequencenodes);
- GraphNode.computeclosure(superset,null);
+ GraphNode.computeclosure(superset,closureset);
try {
GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
} catch (Exception e) {
}
GraphAnalysis ga=new GraphAnalysis(this);
removedset=ga.doAnalysis();
+ if (removedset==null) {
+ System.out.println("Can't generate terminating repair algorithm!");
+ System.exit(-1);
+ }
System.out.println("Removing:");
for(Iterator it=removedset.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
System.out.println(gn.getTextLabel());
}
+
+ superset=new HashSet();
+ superset.addAll(conjunctions);
+ superset.removeAll(removedset);
+ GraphNode.computeclosure(superset,removedset);
+ try {
+ GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
+ } catch (Exception e) {
+ e.printStackTrace();
+ System.exit(-1);
+ }
+
}
void generateconjunctionnodes() {
((Set)conjunctionmap.get(c)).add(gn);
conjtonodemap.put(dnf.get(j),gn);
}
+ for(int j=0;j<c.numQuantifiers();j++) {
+ Quantifier q=c.getQuantifier(j);
+ if (q instanceof SetQuantifier) {
+ SetQuantifier sq=(SetQuantifier)q;
+ VarExpr ve=new VarExpr(sq.getVar());
+ InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
+ DNFConstraint dconst=new DNFConstraint(ip);
+ dconst=dconst.not();
+ TermNode tn=new TermNode(c,dconst.get(0));
+ GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
+ "Conj ("+i+","+j+") "+dconst.get(0).name()
+ ,tn);
+ conjunctions.add(gn);
+ if (!conjunctionmap.containsKey(c))
+ conjunctionmap.put(c,new HashSet());
+ ((Set)conjunctionmap.get(c)).add(gn);
+ conjtonodemap.put(dconst.get(0),gn);
+ } else if (q instanceof RelationQuantifier) {
+ RelationQuantifier rq=(RelationQuantifier)q;
+ VarExpr ve=new VarExpr(rq.y);
+ InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
+ DNFConstraint dconst=new DNFConstraint(ip);
+ dconst=dconst.not();
+ TermNode tn=new TermNode(c,dconst.get(0));
+ GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
+ "Conj ("+i+","+j+") "+dconst.get(0).name()
+ ,tn);
+ conjunctions.add(gn);
+ if (!conjunctionmap.containsKey(c))
+ conjunctionmap.put(c,new HashSet());
+ ((Set)conjunctionmap.get(c)).add(gn);
+ conjtonodemap.put(dconst.get(0),gn);
+ }
+ }
}
}
Constraint constr=tn2.getConstraint();
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
- if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)||
+ if (AbstractInterferes.interferes(sn,dp)||
AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
GraphNode gnconseq=(GraphNode)consequence.get(sn);
-static char rcsid[]="$Id: redblack.c,v 1.1 2004/03/07 22:02:43 bdemsky Exp $";
+static char rcsid[]="$Id: redblack.c,v 1.2 2004/03/10 06:15:03 bdemsky Exp $";
/*
Redblack balanced tree algorithm
/* walk x down the tree */
while(x!=RBNULL) {
- if (low<x->high &&
+ if (low<x->high&&
x->key<high)
return x;
if (x->left!=RBNULL && x->left->max>low)
/*
* $Log: redblack.c,v $
+ * Revision 1.2 2004/03/10 06:15:03 bdemsky
+ *
+ *
+ * Added:
+ * Concrete Interference rule that falsify a rule that quantifies over a set can't
+ * remove the last element of the set.
+ *
+ * Concrete Interference rule that updates that definitely falsify a rule can't modify
+ * the inclusion condition causing a possible addition.
+ *
+ * Intelligence in the GraphAnalysis package that computes must & cant remove sets.
+ * Search through only unique combinations.
+ *
* Revision 1.1 2004/03/07 22:02:43 bdemsky
*
*
projects / repair.git / commitdiff