import java.util.*;
import java.io.*;
import MCC.State;
+import MCC.Compiler;
public class Termination {
HashSet conjunctions;
Hashtable conjunctionmap;
HashSet abstractrepair;
+ HashSet abstractrepairadd;
+
HashSet updatenodes;
HashSet consequencenodes;
Hashtable consequence;
Hashtable abstractadd;
Hashtable abstractremove;
+ Hashtable conjtonodemap;
+ Hashtable predtoabstractmap;
+ Set removedset;
State state;
conjunctions=new HashSet();
conjunctionmap=new Hashtable();
abstractrepair=new HashSet();
+ abstractrepairadd=new HashSet();
scopenodes=new HashSet();
scopesatisfy=new Hashtable();
scopefalsify=new Hashtable();
consequencenodes=new HashSet();
abstractadd=new Hashtable();
abstractremove=new Hashtable();
-
+ conjtonodemap=new Hashtable();
+ predtoabstractmap=new Hashtable();
+ if (!Compiler.REPAIR)
+ return;
generateconjunctionnodes();
generatescopenodes();
HashSet superset=new HashSet();
superset.addAll(conjunctions);
- superset.addAll(abstractrepair);
+ HashSet closureset=new HashSet();
+ // closureset.addAll(updatenodes);
+ //superset.addAll(abstractrepair);
//superset.addAll(updatenodes);
//superset.addAll(scopenodes);
//superset.addAll(consequencenodes);
- //GraphNode.computeclosure(superset);
+ GraphNode.computeclosure(superset,closureset);
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);
+ 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() {
"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);
+ 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);
+ }
}
}
}
}
}
}
+
+ 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);
+ }
+ }
}
}
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);
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);
+ if (!predtoabstractmap.containsKey(dp))
+ predtoabstractmap.put(dp,new HashSet());
+ ((Set)predtoabstractmap.get(dp)).add(gn2);
abstractrepair.add(gn2);
}
}
AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
TermNode tn=new TermNode(ar);
GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
+ if (!predtoabstractmap.containsKey(tp))
+ predtoabstractmap.put(tp,new HashSet());
+ ((Set)predtoabstractmap.get(tp)).add(gn);
abstractrepair.add(gn);
+ abstractrepairadd.add(gn);
abstractadd.put(sd,gn);
DNFPredicate tp2=new DNFPredicate(true,ip);
AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
TermNode tn2=new TermNode(ar2);
GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
+ if (!predtoabstractmap.containsKey(tp2))
+ predtoabstractmap.put(tp2,new HashSet());
+ ((Set)predtoabstractmap.get(tp2)).add(gn2);
abstractrepair.add(gn2);
+ abstractrepairadd.add(gn2);
abstractremove.put(sd,gn2);
}
AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
TermNode tn=new TermNode(ar);
GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
+ if (!predtoabstractmap.containsKey(tp))
+ predtoabstractmap.put(tp,new HashSet());
+ ((Set)predtoabstractmap.get(tp)).add(gn);
abstractrepair.add(gn);
+ abstractrepairadd.add(gn);
abstractadd.put(rd,gn);
DNFPredicate tp2=new DNFPredicate(true,ip);
AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
TermNode tn2=new TermNode(ar2);
GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
+ if (!predtoabstractmap.containsKey(tp2))
+ predtoabstractmap.put(tp2,new HashSet());
+ ((Set)predtoabstractmap.get(tp2)).add(gn2);
abstractrepair.add(gn2);
+ abstractrepairadd.add(gn2);
abstractremove.put(rd,gn2);
}
Rule r=(Rule) state.vRules.get(i);
Vector possiblerules=new Vector();
/* Construct bindings */
- Vector bindings=new Vector();
- constructbindings(bindings, r,true);
-
+ /* No need to construct bindings on remove
+ Vector bindings=new Vector();
+ constructbindings(bindings, r,true);
+ */
for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
GraphNode gn=(GraphNode)scopesatisfy.get(r);
TermNode tn=(TermNode) gn.getOwner();
MultUpdateNode mun=new MultUpdateNode(sn);
TermNode tn2=new TermNode(mun);
GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
- UpdateNode un=new UpdateNode();
- un.addBindings(bindings);
+ UpdateNode un=new UpdateNode(r);
+ // un.addBindings(bindings);
+ // Not necessary
if (j<r.numQuantifiers()) {
/* Remove quantifier */
Quantifier q=r.getQuantifier(j);
continue;
}
}
-
+ if (!un.checkupdates()) /* Make sure we have a good update */
+ continue;
+
mun.addUpdate(un);
GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
if (possiblerules.size()==0)
return;
int[] count=new int[possiblerules.size()];
- while(remains(count,possiblerules)) {
+ while(remains(count,possiblerules,true)) {
MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
TermNode tn=new TermNode(mun);
GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
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);
- un.addBindings(bindings);
+ /* No Need to construct bindings on remove
+ Vector bindings=new Vector();
+ constructbindings(bindings, r,true);
+ un.addBindings(bindings);*/
if (count[i]<r.numQuantifiers()) {
/* Remove quantifier */
Quantifier q=r.getQuantifier(count[i]);
goodflag=false;break;
}
}
+ if (!un.checkupdates()) {
+ goodflag=false;
+ break;
+ }
mun.addUpdate(un);
}
if (goodflag) {
gn.addEdge(e);
updatenodes.add(gn2);
}
- increment(count,possiblerules);
+ increment(count,possiblerules,true);
}
}
- static void increment(int count[], Vector rules) {
+ static void increment(int count[], Vector rules,boolean isremove) {
count[0]++;
for(int i=0;i<(rules.size()-1);i++) {
- if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
+ int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
+ if (count[i]>=num) {
count[i+1]++;
count[i]=0;
} else break;
}
}
- static boolean remains(int count[], Vector rules) {
+ static boolean remains(int count[], Vector rules, boolean isremove) {
for(int i=0;i<rules.size();i++) {
- if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
+ int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
+ if (count[i]>=num) {
return false;
}
}
return true;
}
+ /** This method generates data structure updates to implement the
+ * abstract atomic modification specified by ar. */
+ int modifycount=0;
void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
+ RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
+ ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate();
+ boolean inverted=exprPredicate.inverted();
+ int leftindex=0;
+ int rightindex=1;
+ if (inverted)
+ leftindex=2;
+ else
+ rightindex=2;
+
+
+ Vector possiblerules=new Vector();
+ for(int i=0;i<state.vRules.size();i++) {
+ Rule r=(Rule) state.vRules.get(i);
+ if ((r.getInclusion() instanceof RelationInclusion)&&
+ (rd==((RelationInclusion)r.getInclusion()).getRelation()))
+ possiblerules.add(r);
+ }
+ if (possiblerules.size()==0)
+ return;
+ int[] count=new int[possiblerules.size()];
+ while(remains(count,possiblerules,false)) {
+ MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
+ TermNode tn=new TermNode(mun);
+ GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
+
+ boolean goodflag=true;
+ for(int i=0;i<possiblerules.size();i++) {
+ Rule r=(Rule)possiblerules.get(i);
+ UpdateNode un=new UpdateNode(r);
+ /* No Need to construct bindings on modify */
+
+ int c=count[i];
+ if (!processconjunction(un,r.getDNFGuardExpr().get(c))) {
+ goodflag=false;break;
+ }
+ RelationInclusion ri=(RelationInclusion)r.getInclusion();
+ if (!(ri.getLeftExpr() instanceof VarExpr)) {
+ if (ri.getLeftExpr().isValue()) {
+ Updates up=new Updates(ri.getLeftExpr(),leftindex);
+ un.addUpdate(up);
+ } else
+ goodflag=false;
+ } else {
+ VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
+ if (vd.isGlobal()) {
+ Updates up=new Updates(ri.getLeftExpr(),leftindex);
+ un.addUpdate(up);
+ } else if (inverted)
+ goodflag=false;
+ }
+ if (!(ri.getRightExpr() instanceof VarExpr)) {
+ if (ri.getRightExpr().isValue()) {
+ Updates up=new Updates(ri.getRightExpr(),rightindex);
+ un.addUpdate(up);
+ } else
+ goodflag=false;
+ } else {
+ VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
+ if (vd.isGlobal()) {
+ Updates up=new Updates(ri.getRightExpr(),rightindex);
+ un.addUpdate(up);
+ } else if (!inverted)
+ goodflag=false;
+ }
+
+ if (!un.checkupdates()) {
+ goodflag=false;
+ break;
+ }
+ mun.addUpdate(un);
+ }
+ if (goodflag) {
+ GraphNode.Edge e=new GraphNode.Edge("abstract"+modifycount,gn2);
+ modifycount++;
+ gn.addEdge(e);
+ updatenodes.add(gn2);
+ }
+ increment(count,possiblerules,false);
+ }
}
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) {
SetInclusion si=(SetInclusion)inc;
if (!(si.elementexpr instanceof VarExpr)) {
- Updates up=new Updates(si.elementexpr,0);
- un.addUpdate(up);
+ if (si.elementexpr.isValue()) {
+ Updates up=new Updates(si.elementexpr,0);
+ un.addUpdate(up);
+ } else
+ continue;
} else {
VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
- if (un.getBinding(vd)==null) {
+ if (vd.isGlobal()) {
Updates up=new Updates(si.elementexpr,0);
un.addUpdate(up);
}
} else if (inc instanceof RelationInclusion) {
RelationInclusion ri=(RelationInclusion)inc;
if (!(ri.getLeftExpr() instanceof VarExpr)) {
- Updates up=new Updates(ri.getLeftExpr(),0);
- un.addUpdate(up);
+ if (ri.getLeftExpr().isValue()) {
+ Updates up=new Updates(ri.getLeftExpr(),0);
+ un.addUpdate(up);
+ } else
+ continue;
} else {
VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
- if (un.getBinding(vd)==null) {
+ if (vd.isGlobal()) {
Updates up=new Updates(ri.getLeftExpr(),0);
un.addUpdate(up);
}
}
if (!(ri.getRightExpr() instanceof VarExpr)) {
- Updates up=new Updates(ri.getRightExpr(),1);
- un.addUpdate(up);
+ if (ri.getRightExpr().isValue()) {
+ Updates up=new Updates(ri.getRightExpr(),1);
+ un.addUpdate(up);
+ } else
+ continue;
} else {
VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
- if (un.getBinding(vd)==null) {
+ if (vd.isGlobal()) {
Updates up=new Updates(ri.getRightExpr(),1);
un.addUpdate(up);
}
GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
if (processquantifers(gn2,un, r)&&debugdd()&&
- processconjunction(un,ruleconj)) {
+ 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);
}
} else {
System.out.println(e.getClass().getName());
- throw new Error("Error #213");
+ throw new Error("Unrecognized Expr");
}
}
return okay;
projects / repair.git / blobdiff