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();
/* 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;
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))) {
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++) {
doesn't exist.*/
}
- if (interferes(update,dexpr))
- return true;
+ if (interferes(update,dexpr)) {
+ if (Compiler.DEBUGGRAPH)
+ System.out.println("CASE 3");
+
+ return true;
+ }
}
- }
+ }
}
}
return false;
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();