if (!leftside.equals(mapping,e2))
return false;
}
+
+
/* Prune precondition using any ar's in the same conjunction */
adjustcondition(precondition, ar);
Conjunction conj=findConjunction(repair_c.getDNFConstraint(),ar.getPredicate());
+
+ /* We don't interfere with the same constraint, if there
+ aren't any shared state problems between different
+ bindings (which we've already checked for), and its a
+ different conjunction. Because we wouldn't have repair it
+ if it wasn't already broken. Doesn't appear to be needed,
+ the cycle algorithm will just eliminate one of the nodes.
+
+ if (repair_c==interfere_c) {
+ if (conj!=findConjunction(interfere_c.getDNFConstraint(),interfere_pred))
+ return true;
+ }*/
+
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
Set s=(Set)termination.predtoabstractmap.get(dp);
generateconjunctionnodes();
constraintdependence=new ConstraintDependence(state,this);
+ debugmsg("Generating scope nodes");
generatescopenodes();
+ debugmsg("Generating repair nodes");
generaterepairnodes();
+ debugmsg("Generating data structure nodes");
generatedatastructureupdatenodes();
+ debugmsg("Generating compensation nodes");
generatecompensationnodes();
-
+ debugmsg("Generating abstract edges");
generateabstractedges();
+ debugmsg("Generating scope edges");
generatescopeedges();
+ debugmsg("Generating update edges");
generateupdateedges();
HashSet superset=new HashSet();
superset.addAll(conjunctions);
HashSet closureset=new HashSet();
-
+ debugmsg("Computing closure");
GraphNode.computeclosure(superset,closureset);
try {
GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
} else {
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
- if (getConstraint(gn)!=null&&
- abstractinterferes.interferemodifies(ar,getConstraint(gn),dp,cons))
- continue;
- if (abstractinterferes.interfereswithpredicate(ar,dp)) {
+ if (!abstractinterferes.interfereswithpredicate(ar,dp))
+ continue;
+ if (getConstraint(gn)==null||
+ !abstractinterferes.interferemodifies(ar,getConstraint(gn),dp,cons)) {
GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
gn.addEdge(e);
break;