package MCC.IR;
import java.util.*;
+import MCC.Compiler;
public class ConcreteInterferes {
Termination termination;
* model definition rule r. */
public boolean interferes(MultUpdateNode mun, Rule r, boolean satisfy) {
-
+
// A rule that adds something to a set can't be falsified by
// an update that is only performed if the set is empty
- if (!initialinterferes(mun,r,satisfy))
+ if (!initialinterferes(mun,r,satisfy))
return false;
for(int i=0;i<mun.numUpdates();i++) {
for (int j=0;j<un.numUpdates();j++) {
Updates update=un.getUpdate(j);
//Abstract updates don't have concrete interference1
- if (update.isAbstract())
+ if (update.isAbstract())
continue;
-
+
DNFRule drule=satisfy?r.getDNFNegGuardExpr():r.getDNFGuardExpr();
Descriptor updated_des=update.getDescriptor();
assert updated_des!=null;
/* Test to see if the update only effects new
objects and we're only testing for falsifying
model definition rules. */
-
+
if ((!satisfy)&&updateonlytonewobject(mun,un,update))
continue;
-
// See if the update interferes with the inclusion
// condition for the rule
if (r.getInclusion().usesDescriptor(updated_des)) {
node already models the action of this
update. */
- if ((un.getRule()==r)&&
+ if ((un.getRule()==r)&&
(((mun.op==MultUpdateNode.ADD)&&satisfy)
||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
||(mun.op==MultUpdateNode.MODIFY))) {
} else throw new Error();
}
+ if ((un.getRule()==r)&&
+ ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
+ modifiesremoves(mun,un,r)) {
+ Inclusion inclusion=r.getInclusion();
+ if (inclusion instanceof RelationInclusion) {
+ RelationInclusion ri=(RelationInclusion)inclusion;
+ if ((!testdisjoint(update,r,ri.getLeftExpr()))&&
+ (!testdisjoint(update,r,ri.getRightExpr())))
+ ok=true; /* Update is specific to
+ given binding of the rule,
+ and adds are only performed
+ if the removal is desired or
+ the tuple doesn't exist.*/
+ }
+ }
+
if (!ok) {
if (satisfy) {
/** Check to see if the update definitely falsifies r, thus
* can't accidentally satisfy it r. */
- if (interferesinclusion(un, update, r))
+ if (interferesinclusion(un, update, r)) {
+ if (Compiler.DEBUGGRAPH)
+ System.out.println("CASE 1");
return true;
- } else
- return true; /* Interferes with inclusion condition */
+ }
+ } else {
+ if (Compiler.DEBUGGRAPH)
+ System.out.println("CASE 2");
+
+ return true; /* Interferes with inclusion condition */
+ }
}
}
-
+
for(int k=0;k<drule.size();k++) {
RuleConjunction rconj=drule.get(k);
for(int l=0;l<rconj.size();l++) {
intended one, so we're
okay */
}
- if (interferes(update,dexpr))
- return true;
+ if ((un.getRule()==r)&&
+ ((mun.op==MultUpdateNode.ADD)&&!satisfy)&&
+ modifiesremoves(mun,un,r)) {
+ if (!testdisjoint(update,r,dexpr.getExpr()))
+ continue; /* Update is specific to
+ given binding of the
+ rule, and adds are only
+ performed if the removal
+ is desired or the tuple
+ doesn't exist.*/
+ }
+
+ if (interferes(update,dexpr)) {
+ if (Compiler.DEBUGGRAPH)
+ System.out.println("CASE 3");
+
+ return true;
+ }
}
- }
+ }
}
}
return false;
}
-
+
+
+ static private boolean modifiesremoves(MultUpdateNode mun,UpdateNode un, Rule r) {
+ AbstractRepair ar=mun.getRepair();
+ boolean inverted=ar.getPredicate().getPredicate().inverted();
+
+ if (ar.getType()!=AbstractRepair.MODIFYRELATION)
+ return false;
+ RelationInclusion ri=(RelationInclusion)r.getInclusion();
+ Expr e=inverted?ri.getRightExpr():ri.getLeftExpr();
+ while(e instanceof CastExpr) {
+ e=((CastExpr)e).getExpr();
+ }
+ if (!(e instanceof VarExpr))
+ return false;
+ VarExpr ve=(VarExpr)e;
+ if (ve.isValue())
+ return false;
+ return true;
+ }
+
static private boolean updateonlytonewobject(MultUpdateNode mun, UpdateNode un, Updates updates) {
AbstractRepair ar=mun.getRepair();
if ((ar!=null)&&(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION))
}
}
}
-
+
return false;
}
/** This method tries to show that if the Update update from the
* UpdateNode un changes the value of the inclusion constraint
* that it falsifies the guard of model definition rule. */
-
+
static private boolean interferesinclusion(UpdateNode un, Updates update, Rule r) {
Descriptor updated_des=update.getDescriptor();
Inclusion inclusion=r.getInclusion();
/* 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();
boolean varok=true;
Set vars=rexpr.freeVars();
- if (vars!=null)
+ if (vars!=null)
for(Iterator it=vars.iterator();it.hasNext();) {
VarDescriptor vd=(VarDescriptor) it.next();
if (!vd.isGlobal()) {
}
}
}
-
+
if (!varok)
continue;
rexpr.equals(remap,update.getRightExpr())) {
match=true;
break;
- }
+ }
}
- }
+ }
}
if (!match) {
good=false;
return false; /* Can't accidentally interfere with other bindings if there aren't any! */
boolean firstfield=true;
-
+
while(true) {
if (update_e instanceof CastExpr)
}
return null;
}
-
+
/** This function checks to see if an update is only performed if
* a given set (or image set produced by a relation) is empty, and
* the algorithm is computing whether the update may falsify a
if (ep.getType()!=ExprPredicate.SIZE)
return true;
Opcode op=Opcode.translateOpcode(negated,ep.getOp());
-
+
if (((op==Opcode.EQ)&&(ep.rightSize()==1))|| //(=1)
((op==Opcode.NE)&&(ep.rightSize()==0))|| //(!=0)
((op==Opcode.GT)&&(ep.rightSize()==0))|| //(>0)
for (int j=0;j<un.numUpdates();j++) {
Updates update=un.getUpdate(j);
//Abstract updates don't have concrete interference1
- if (update.isAbstract())
+ if (update.isAbstract())
continue;
if (testdisjoint(update, r, r.getGuardExpr()))
return true;
there is no interference. */
if (!dexpr.getExpr().usesDescriptor(descriptor))
return false;
-
+
if (update.isExpr()) {
/* We need to pair the variables */
Set vars=update.getRightExpr().freeVars();
projects / repair.git / blobdiff