+ public ConcreteInterferes(Termination t) {
+ this.termination=t;
+ }
+
+ /** Returns true if the data structure updates performed by mun
+ * may increase (or decrease if satisfy=false) the scope of the
+ * 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))
+ return false;
+
+ for(int i=0;i<mun.numUpdates();i++) {
+ UpdateNode un=mun.getUpdate(i);
+ for (int j=0;j<un.numUpdates();j++) {
+ Updates update=un.getUpdate(j);
+ //Abstract updates don't have concrete interference1
+ 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)) {
+ boolean ok=false;
+
+ /* If the update is for this rule, and the effect
+ is the intended effect, and the update only
+ effects one binding, then the abstract repair
+ node already models the action of this
+ update. */
+
+ if ((un.getRule()==r)&&
+ (((mun.op==MultUpdateNode.ADD)&&satisfy)
+ ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
+ ||(mun.op==MultUpdateNode.MODIFY))) {
+ 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;
+ } else if (inclusion instanceof SetInclusion) {
+ SetInclusion si=(SetInclusion)inclusion;
+ if (!testdisjoint(update,r,si.getExpr()))
+ ok=true;
+ } 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))
+ return true;
+ } else
+ 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++) {
+ DNFExpr dexpr=rconj.get(l);
+ /* See if update interferes w/ dexpr */
+ if ((un.getRule()==r)&&
+ (((mun.op==MultUpdateNode.ADD)&&satisfy)
+ ||((mun.op==MultUpdateNode.REMOVE)&&!satisfy)
+ ||(mun.op==MultUpdateNode.MODIFY))) {
+ if (!testdisjoint(update,r,dexpr.getExpr()))
+ continue; /* Update is specific to
+ given binding of the
+ rule, and effect is the
+ intended one, so we're
+ okay */
+ }
+ 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))
+ 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))
+ for(int i=0;i<un.numUpdates();i++) {
+ Updates u=un.getUpdate(i);
+ if (u.getType()==Updates.POSITION&&
+ ar.isNewObject(u.getRightPos()==0)) {
+ Expr newleftexpr=u.getLeftExpr();
+ Expr leftexpr=updates.getLeftExpr();
+ boolean foundfield=false;
+ while(true) {
+ if (leftexpr.equals(null,newleftexpr)) {
+ if (foundfield)
+ return true;
+ else
+ break;
+ } else if (leftexpr instanceof DotExpr) {
+ if (!foundfield) {
+ foundfield=true;
+ } else {
+ if (((DotExpr)leftexpr).isPtr())
+ break; //if its not a pointer, we're still in the structure
+ }
+ leftexpr=((DotExpr)leftexpr).getExpr();
+ } else if (leftexpr instanceof CastExpr) {
+ leftexpr=((CastExpr)leftexpr).getExpr();
+ } else
+ break;
+ }
+ }
+ }
+
+ 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) {