Set removedset;
ComputeMaxSize maxsize;
State state;
+ AbstractInterferes abstractinterferes;
+
public Termination(State state) {
this.state=state;
if (!Compiler.REPAIR)
return;
+
for(int i=0;i<state.vRules.size();i++)
System.out.println(state.vRules.get(i));
for(int i=0;i<state.vConstraints.size();i++)
maxsize=new ComputeMaxSize(state);
+ abstractinterferes=new AbstractInterferes(this);
generateconjunctionnodes();
generatescopenodes();
generaterepairnodes();
}
}
-
+
+
+ /** This method generates a node for each conjunction in the DNF form of each constraint.
+ * It also converts the quantifiers into conjunctions also - constraints can be satisfied by
+ * removing items from the sets and relations they are quantified over */
void generateconjunctionnodes() {
Vector constraints=state.vConstraints;
+ // Constructs conjunction nodes
for(int i=0;i<constraints.size();i++) {
Constraint c=(Constraint)constraints.get(i);
DNFConstraint dnf=c.dnfconstraint;
((Set)conjunctionmap.get(c)).add(gn);
conjtonodemap.put(dnf.get(j),gn);
}
+ // Construct quantifier "conjunction" nodes
for(int j=0;j<c.numQuantifiers();j++) {
Quantifier q=c.getQuantifier(j);
if (q instanceof SetQuantifier) {
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
if (AbstractInterferes.interferes(ar,cons)||
- AbstractInterferes.interferes(ar,dp)) {
+ abstractinterferes.interferes(ar,dp)) {
GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
gn.addEdge(e);
break;
Constraint constr=tn2.getConstraint();
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
- if (AbstractInterferes.interferes(sn,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);
}
}
- /* Generates the abstract repair nodes */
+ /** This method generates the abstract repair nodes. */
void generaterepairnodes() {
/* Generate repairs of conjunctions */
for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
}
}
- static void increment(int count[], Vector rules,boolean isremove) {
+ static private void increment(int count[], Vector rules,boolean isremove) {
count[0]++;
for(int i=0;i<(rules.size()-1);i++) {
int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
}
}
- static boolean remains(int count[], Vector rules, boolean isremove) {
+ static private boolean remains(int count[], Vector rules, boolean isremove) {
for(int i=0;i<rules.size();i++) {
int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
if (count[i]>=num) {
increment(count,possiblerules,false);
}
}
-
+ /** This method constructs bindings for an update using rule
+ * r. The boolean flag isremoval indicates that the update
+ * performs a removal. The function returns true if it is able to
+ * generate a valid set of bindings and false otherwise. */
boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
boolean goodupdate=true;
SetDescriptor set=null;
if (q instanceof SetQuantifier) {
vd=((SetQuantifier)q).getVar();
- } else
+ set=((SetQuantifier)q).getSet();
+ } else {
vd=((ForQuantifier)q).getVar();
+ }
if(inc instanceof SetInclusion) {
SetInclusion si=(SetInclusion)inc;
if ((si.elementexpr instanceof VarExpr)&&
/* Can solve for v */
Binding binding=new Binding(vd,0);
bindings.add(binding);
- } else
+ } else {
goodupdate=false;
+ }
} else if (inc instanceof RelationInclusion) {
RelationInclusion ri=(RelationInclusion)inc;
boolean f1=true;
} else throw new Error("Inclusion not recognized");
if (!goodupdate)
if (isremoval) {
- Binding binding=new Binding(vd);
+ /* Removals don't need bindings anymore
+ Binding binding=new Binding(vd);
+ bindings.add(binding);*/
+ goodupdate=true;
+ } else {
+ /* Create new element to bind to */
+ Binding binding=new Binding(vd,set,createorsearch(set));
bindings.add(binding);
goodupdate=true;
- } else
- break;
+ //FIXME
+ }
} else if (q instanceof RelationQuantifier) {
RelationQuantifier rq=(RelationQuantifier)q;
for(int k=0;k<2;k++) {
} else throw new Error("Inclusion not recognized");
if (!goodupdate)
if (isremoval) {
- Binding binding=new Binding(vd);
- bindings.add(binding);
+ /* Removals don't need bindings anymore
+ Binding binding=new Binding(vd);
+ bindings.add(binding);*/
goodupdate=true;
} else
break;
return goodupdate;
}
+ /** Returns true if we search for an element from sd
+ * false if we create an element for sd */
+ private boolean createorsearch(SetDescriptor sd) {
+ return false;
+ }
+
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());
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());
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");
if (!constructbindings(bindings,r,false))
continue;
- //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++) {
}
//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");
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()&&
+ if (processquantifers(gn2,un, r)&&
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");
- return true;
- }
-
+
+ /** Adds updates that add an item to the appropriate set or
+ * relation quantified over by the model definition rule.. */
+
boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
Inclusion inc=r.getInclusion();
for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
} else {
return false;
}
-
+
} else if (q instanceof SetQuantifier) {
SetQuantifier sq=(SetQuantifier)q;
ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
projects / repair.git / blobdiff