Stack workset=new Stack();
HashSet closureset=new HashSet();
boolean needcyclecheck=false;
- HashSet cantremovetrans=new HashSet();
+ HashSet dependent=new HashSet();
+
+ /* Compute dependent set */
+ workset.push(gn);
+ while(!workset.empty()) {
+ GraphNode gn2=(GraphNode)workset.pop();
+ for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
+ GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
+ if (removed.contains(gn3))
+ continue;
+ if (!termination.conjunctions.contains(gn3)&&!dependent.contains(gn3)) {
+ dependent.add(gn3);
+ workset.push(gn3);
+ }
+ }
+ }
+
+ /* Compute the closure set */
workset.push(gn);
while(!workset.empty()) {
GraphNode gn2=(GraphNode)workset.pop();
if (!closureset.contains(gn2)) {
closureset.add(gn2);
- boolean goodoption=false;
for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
if (removed.contains(gn3))
continue;
- if (((cantremove.contains(gn2)||!couldremove.contains(gn2))
- &&termination.conjunctions.contains(gn2))||
- cantremovetrans.contains(gn2))
- cantremovetrans.add(gn3);
-
- if (termination.abstractrepair.contains(gn3)||
- termination.conjunctions.contains(gn3)||
- termination.updatenodes.contains(gn3)) {
- /** Check for cycles if the graphnode can't
- * be removed (we know we aren't introducing
- * new things to repair). */
- if ((!termination.abstractrepair.contains(gn3)&&
- cantremove.contains(gn3))||
- cantremovetrans.contains(gn3)) {
- needcyclecheck=true;
- } else return false;
- }
- if ((!couldremove.contains(gn3))||cantremove.contains(gn3))
- goodoption=true;
workset.push(gn3);
}
- if (!goodoption) {
- if (termination.scopenodes.contains(gn2))
- return false;
- }
}
}
- if (needcyclecheck) {
- Set cycles=GraphNode.findcycles(closureset);
- for(Iterator it=cycles.iterator();it.hasNext();) {
- GraphNode gn2=(GraphNode)it.next();
- if (termination.abstractrepair.contains(gn2)||
- termination.conjunctions.contains(gn2)||
- termination.updatenodes.contains(gn2))
- return false;
+
+ /* Check for harmful cycles through gn */
+ Set cycles=GraphNode.findcycles(closureset);
+ if (cycles.contains(gn))
+ return false;
+
+ /* Check for harmful cycles being introduced in dependent nodes */
+ cycles=GraphNode.findcycles(dependent);
+ for(Iterator it=cycles.iterator();it.hasNext();) {
+ GraphNode gn2=(GraphNode)it.next();
+ if (termination.abstractrepair.contains(gn2)||
+ termination.conjunctions.contains(gn2)||
+ termination.updatenodes.contains(gn2))
+ return false;
+ }
+
+ /* Make sure all abstractrepairs/consequence nodes in the dependent nodes
+ are well formed. */
+ outerloop:
+ for(Iterator it=dependent.iterator();it.hasNext();) {
+ GraphNode gn2=(GraphNode)it.next();
+ if (termination.abstractrepair.contains(gn2)||
+ termination.scopenodes.contains(gn2)) {
+ boolean ismodify=false;
+ int numadd=0;
+ int numremove=0;
+
+ if (termination.abstractrepair.contains(gn2)&&
+ ((TermNode)gn2.getOwner()).getAbstract().getType()==AbstractRepair.MODIFYRELATION)
+ ismodify=true;
+
+ innerloop:
+ for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
+ GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
+ if (removed.contains(gn3))
+ continue innerloop;
+ if (cantremove.contains(gn3)||
+ !couldremove.contains(gn3)) {
+ if (ismodify) {
+ TermNode tn3=(TermNode)gn3.getOwner();
+ MultUpdateNode mun=tn3.getUpdate();
+ if (mun.getType()==MultUpdateNode.ADD)
+ numadd++;
+ if (mun.getType()==MultUpdateNode.REMOVE)
+ numremove++;
+ if (mun.getType()==MultUpdateNode.MODIFY)
+ continue outerloop;
+ if ((numadd>0)&&(numremove>0||!((TermNode)gn2.getOwner()).getAbstract().needsRemoves(termination.state)))
+ continue outerloop;
+ } else
+ if (termination.consequence.contains(gn3)||
+ termination.updatenodes.contains(gn3))
+ continue outerloop;
+ }
+ }
+ return false;
}
}
return true;
for(Iterator it=termination.consequencenodes.iterator();it.hasNext();) {
GraphNode gn=(GraphNode) it.next();
if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
- couldremove.remove(gn);
+ couldremove.remove(gn);
}
}
for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
GraphNode gn=(GraphNode) it.next();
- if (safetransclosure(gn, mustremove,cantremove, cantremove)) {
- couldremove.remove(gn);
+ if (safetransclosure(gn, mustremove,cantremove, couldremove)) {
+ couldremove.remove(gn);
}
}
GraphNode gn=(GraphNode) it.next();
if (mustremove.contains(gn)||cantremove.contains(gn))
continue;
+ if (!safetransclosure(gn, mustremove,cantremove, couldremove))
+ continue;
boolean allgood=true;
for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
assert tn2.getType()==TermNode.ABSTRACT;
boolean foundupdate=false;
for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
- GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();
+ GraphNode gn3=((GraphNode.Edge)edgeit2.next()).getTarget();
if (!couldremove.contains(gn3)&&!mustremove.contains(gn3)) {
TermNode tn3=(TermNode)gn3.getOwner();
if (tn3.getType()==TermNode.UPDATE)
if (!foundupdate)
allgood=false;
}
- if (allgood)
+ if (allgood) {
couldremove.remove(gn);
+ if (Compiler.PRUNEQUANTIFIERS) {
+ TermNode tn=(TermNode)gn.getOwner();
+ Constraint constr=tn.getConstraint();
+ for(Iterator consit=((Set)termination.conjunctionmap.get(constr)).iterator();consit.hasNext();) {
+ GraphNode gn4=(GraphNode)consit.next();
+ TermNode tn4=(TermNode)gn4.getOwner();
+ if (tn4.getquantifiernode()) {
+ mustremove.add(gn4); /* This node is history */
+ System.out.println("Eliminating: "+gn4.getTextLabel());
+ }
+ }
+ }
+ }
}
/* Look for constraints which can only be satisfied one way */
-
+
Vector constraints=termination.state.vConstraints;
for(int i=0;i<constraints.size();i++) {
Constraint c=(Constraint)constraints.get(i);
}
- /* Search through conjunction which must be satisfied, and attempt
- to generate appropriate repair actions.
- */
+ /* Search through conjunction nodes which must be
+ satisfied, and see if there are any data structure
+ updates that must exist. */
+
HashSet newset=new HashSet();
for(Iterator cit=cantremove.iterator();cit.hasNext();) {
GraphNode gn=(GraphNode)cit.next();
change=true;
}
}
-
+
if (Compiler.AGGRESSIVESEARCH) {
/* Aggressively remove compensation nodes */
for(Iterator scopeit=termination.scopenodes.iterator();scopeit.hasNext();) {
}
System.out.println("Cycle through conjunction "+gn.getTextLabel() +" which can't be removed.");
+ System.out.println("CANTREMOVE");
+ for(Iterator it2=cantremove.iterator();it2.hasNext();) {
+ GraphNode gn2=(GraphNode)it2.next();
+ System.out.println(gn2.getTextLabel());
+ }
+ System.out.println("MUSTREMOVE");
+ for(Iterator it2=mustremove.iterator();it2.hasNext();) {
+ GraphNode gn2=(GraphNode)it2.next();
+ System.out.println(gn2.getTextLabel());
+ }
return null; // Out of luck
}
}
/* Searches individual conjunctions + abstract action +updates for cycles */
for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
- boolean foundnocycle=false;
for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
+ boolean foundnocycle=false;
+
GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
GraphNode gn2=e.getTarget();
TermNode tn2=(TermNode)gn2.getOwner();
AbstractRepair ar=tn2.getAbstract();
boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
int numadd=0;int numremove=0;
-
+
for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
GraphNode gn3=e2.getTarget();
if (!containsgn3)
cantremove.remove(gn3);
}
- if (ismodify&&((numadd==0)||(numremove==0))) {
+ if (ismodify&&((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state)))) {
for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
GraphNode gn3=e2.getTarget();
mustremove.add(gn3);
}
}
- }
- if(!foundnocycle) {
- if (!mustremove.contains(gn)) {
- change=true;
- mustremove.add(gn);
- }
- }
+
+ if(!foundnocycle) {
+ if (!mustremove.contains(gn)) {
+ change=true;
+ mustremove.add(gn);
+ }
+ }
+ }
}
/* Searches scope nodes + compensation nodes */
for(Iterator it=termination.scopenodes.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
- int count=0;
if (nodes.contains(gn)) {
for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
GraphNode gn2=e.getTarget();
TermNode tn2=(TermNode)gn2.getOwner();
-
- if ((tn2.getType()==TermNode.CONSEQUENCE)&&
- !mustremove.contains(gn2))
- count++;
-
if (tn2.getType()!=TermNode.UPDATE)
continue;
boolean containsgn2=cantremove.contains(gn2);
cantremove.add(gn);
cantremove.add(gn2);
-
+
Set cycle=GraphNode.findcycles(cantremove);
if (cycle.contains(gn2)) {
if (!mustremove.contains(gn2)) {
change=true;
mustremove.add(gn2);
}
- } else {
- if (!mustremove.contains(gn2))
- count++;
}
if (!containsgn)
cantremove.remove(gn);
if (!containsgn2)
cantremove.remove(gn2);
}
-
- if (count==1) {
- for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
- GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
- GraphNode gn2=e.getTarget();
- TermNode tn2=(TermNode)gn2.getOwner();
- if ((tn2.getType()==TermNode.UPDATE||tn2.getType()==TermNode.CONSEQUENCE)&&
- !mustremove.contains(gn2)) {
- if (!cantremove.contains(gn2)) {
- cantremove.add(gn2);
- change=true;
- }
- }
- }
- }
}
}
couldremove.removeAll(mustremove);
couldremove.removeAll(cantremove);
-
+
Vector couldremovevector=new Vector();
couldremovevector.addAll(couldremove);
Vector combination=new Vector();
e.printStackTrace();
System.exit(-1);
}
-
+
System.out.println("Searching set of "+couldremove.size()+" nodes.");
System.out.println("Eliminated must "+mustremove.size()+" nodes");
System.out.println("Eliminated cant "+cantremove.size()+" nodes");
GraphNode gn=(GraphNode)it.next();
System.out.println(gn.getTextLabel());
}
-
-
+
+ System.out.println("==================================================");
while(true) {
if (illegal(combination,couldremovevector))
break;
Set combinationset=buildset(combination,couldremovevector);
+ System.out.println("---------------------------");
+ for(Iterator it=combinationset.iterator();it.hasNext();) {
+ System.out.println(((GraphNode)it.next()).getTextLabel());
+ }
+ System.out.println("---------------------------");
checkmodify(combinationset);
combinationset.addAll(mustremove);
if (combinationset!=null) {
- System.out.println("Checkabstract="+checkAbstract(combinationset));
- System.out.println("Checkrepairs="+checkRepairs(combinationset));
- System.out.println("Checkall="+checkAll(combinationset));
-
- if (checkAbstract(combinationset)==0&&
- checkRepairs(combinationset)==0&&
- checkAll(combinationset)==0) {
+ int checkabstract=checkAbstract(combinationset);
+ int checkrep=checkRepairs(combinationset);
+ int checkall=checkAll(combinationset);
+
+ System.out.println("Checkabstract="+checkabstract);
+ System.out.println("Checkrepairs="+checkrep);
+ System.out.println("Checkall="+checkall);
+
+ if (checkabstract==0&&
+ checkrep==0&&
+ checkall==0) {
return combinationset;
}
}
if (!removednodes.contains(gn2)&&
tn2.getType()==TermNode.UPDATE) {
MultUpdateNode mun=tn2.getUpdate();
-
+
if (mun.getType()==MultUpdateNode.ADD)
numadd++;
if (mun.getType()==MultUpdateNode.REMOVE)
numremove++;
}
}
- if ((numadd==0)||(numremove==0)) {
+ if ((numadd==0)||(numremove==0&&ar.needsRemoves(termination.state))) {
for(Iterator it2=gn.edges();it2.hasNext();) {
GraphNode.Edge edge=(GraphNode.Edge)it2.next();
GraphNode gn2=edge.getTarget();
foundrepair=true;
}
}
- if (!foundrepair)
+ if (!foundrepair) {
return ERR_NOREPAIR;
+ }
}
tset.addAll(termination.consequencenodes);
abstractnodes.retainAll(tset);
Set cycles=GraphNode.findcycles(abstractnodes);
-
+
for(Iterator it=cycles.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
System.out.println("NODE: "+gn.getTextLabel());
projects / repair.git / blobdiff