for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
- if (!cantremove.contains(gn)) {
- cantremove.add(gn);
- Set cycle=GraphNode.findcycles(cantremove);
- if (cycle.contains(gn)) {
- if (!mustremove.contains(gn)) {
- change=true;
- mustremove.add(gn);
+ boolean foundnocycle=false;
+
+ 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.ABSTRACT)
+ continue;
+ for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
+ GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
+ GraphNode gn3=e2.getTarget();
+ TermNode tn3=(TermNode)gn3.getOwner();
+ if (tn3.getType()!=TermNode.UPDATE)
+ continue;
+ boolean containsgn=cantremove.contains(gn);
+ boolean containsgn3=cantremove.contains(gn3);
+ cantremove.add(gn);
+ cantremove.add(gn3);
+ Set cycle=GraphNode.findcycles(cantremove);
+ if (cycle.contains(gn3)) {
+ if (!mustremove.contains(gn3)) {
+ change=true;
+ mustremove.add(gn3);
+ }
}
+ if (!mustremove.contains(gn3)&&!cycle.contains(gn)) {
+ foundnocycle=true;
+ }
+ if (!containsgn)
+ cantremove.remove(gn);
+ if (!containsgn3)
+ cantremove.remove(gn3);
+ }
+ }
+ if(!foundnocycle) {
+ if (!mustremove.contains(gn)) {
+ change=true;
+ mustremove.add(gn);
}
- cantremove.remove(gn);
}
}
couldremove.removeAll(mustremove);
continue; //recalculate
System.out.println("Searching set of "+couldremove.size()+" nodes.");
- System.out.println("Eliminated "+mustremove.size()+" nodes");
+ System.out.println("Eliminated must "+mustremove.size()+" nodes");
+ System.out.println("Eliminated cant "+cantremove.size()+" nodes");
System.out.println("Searching following set:");
for(Iterator it=couldremove.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
private String label;
private GraphNode target;
+ private GraphNode source;
private String dotnodeparams = new String();
public Edge(String label, GraphNode target) {
return label;
}
+ public void setSource(GraphNode s) {
+ this.source=s;
+ }
+
+ public GraphNode getSource() {
+ return source;
+ }
+
public GraphNode getTarget() {
return target;
}
int discoverytime = -1;
int finishingtime = -1; /* used for searches */
+ int scc = -1;
+
Vector edges = new Vector();
+ Vector inedges = new Vector();
String nodelabel;
String textlabel;
NodeStatus status = UNVISITED;
return edges.iterator();
}
+ public Iterator inedges() {
+ return inedges.iterator();
+ }
+
public void addEdge(Edge newedge) {
+ newedge.setSource(this);
edges.addElement(newedge);
+ GraphNode tonode=newedge.getTarget();
+ tonode.inedges.addElement(newedge);
}
- public void reset() {
- discoverytime = -1;
- finishingtime = -1;
- status = UNVISITED;
+ void reset() {
+ discoverytime = -1;
+ finishingtime = -1;
+ status = UNVISITED;
}
- public void discover(int time) {
- discoverytime = time;
- status = PROCESSING;
+ void resetscc() {
+ status = UNVISITED;
+ scc = -1;
}
- public void finish(int time) {
+ public int getSCC() {
+ return scc;
+ }
+
+ void setSCC(int s) {
+ scc=s;
+ }
+
+ void discover(int time) {
+ discoverytime = time;
+ status = PROCESSING;
+ }
+
+ void finish(int time) {
assert status == PROCESSING;
- finishingtime = time;
+ finishingtime = time;
status = FINISHED;
}
+ /** Returns finishing time for dfs */
+
public int getFinishingTime() {
- return finishingtime;
+ return finishingtime;
}
return true; /* found cycle */
}
+ public static class SCC {
+ boolean hascycles;
+ HashMap map;
+ int numscc;
+ public SCC(boolean hascycles, HashMap map,int numscc) {
+ this.hascycles=hascycles;
+ this.map=map;
+ this.numscc=numscc;
+ }
+
+ public boolean hasCycles() {
+ return hascycles;
+ }
+
+ public int numSCC() {
+ return numscc;
+ }
+
+ public Set getSCC(int i) {
+ Integer scc=new Integer(i);
+ return (Set)map.get(scc);
+ }
+
+ boolean hascycle(int i) {
+ Integer scc=new Integer(i);
+ Set s=(Set)map.get(scc);
+ if (s.size()>1)
+ return true;
+ Object [] array=s.toArray();
+ GraphNode gn=(GraphNode)array[0];
+ for(Iterator it=gn.edges();it.hasNext();) {
+ Edge e=(Edge)it.next();
+ if (e.getTarget()==gn)
+ return true; /* Self Cycle */
+ }
+ return false;
+ }
+ }
+
/**
* DFS encapsulates the depth first search algorithm
*/
public static class DFS {
int time = 0;
+ int sccindex = 0;
Collection nodes;
+ Vector finishingorder=null;
+ HashMap sccmap;
private DFS(Collection nodes) {
this.nodes = nodes;
}
+ public static SCC computeSCC(Collection nodes) {
+ if (nodes==null) {
+ throw new NullPointerException();
+ }
+ DFS dfs=new DFS(nodes);
+ dfs.sccmap=new HashMap();
+ dfs.finishingorder=new Vector();
+ boolean hascycles=dfs.go();
+ for (Iterator it = nodes.iterator();it.hasNext();) {
+ GraphNode gn = (GraphNode) it.next();
+ gn.resetscc();
+ }
+ for(int i=dfs.finishingorder.size()-1;i>=0;i--) {
+ GraphNode gn=(GraphNode)dfs.finishingorder.get(i);
+ if (gn.getStatus() == UNVISITED) {
+ dfs.dfsprev(gn);
+ dfs.sccindex++; /* Increment scc index */
+ }
+ }
+ return new SCC(hascycles,dfs.sccmap,dfs.sccindex);
+ }
+
+ void dfsprev(GraphNode gn) {
+ if (gn.getStatus()==FINISHED||!nodes.contains(gn))
+ return;
+ gn.setStatus(FINISHED);
+ gn.setSCC(sccindex);
+ Integer i=new Integer(sccindex);
+ if (!sccmap.containsKey(i))
+ sccmap.put(i,new HashSet());
+ ((Set)sccmap.get(i)).add(gn);
+ for(Iterator edgeit=gn.inedges();edgeit.hasNext();) {
+ Edge e=(Edge)edgeit.next();
+ GraphNode gn2=e.getSource();
+ dfsprev(gn2);
+ }
+ }
+
public static boolean depthFirstSearch(Collection nodes) {
if (nodes == null) {
throw new NullPointerException();
private boolean dfs(GraphNode gn) {
boolean acyclic=true;
- gn.discover(time++);
+ gn.discover(time++);
Iterator edges = gn.edges();
while (edges.hasNext()) {
acyclic=false;
}
}
-
+ if (finishingorder!=null)
+ finishingorder.add(gn);
gn.finish(time++);
return acyclic;
}
boolean needDR(RelationDescriptor rd,boolean isdomain) {
Vector rules=state.vRules;
SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
+ if (sd instanceof ReservedSetDescriptor)
+ return false;
for(int i=0;i<rules.size();i++) {
Rule r=(Rule)rules.get(i);
if ((r.numQuantifiers()==1)&&
}
return true;
}
+ /** This method generates data structure updates to implement the
+ * abstract atomic modification specified by ar. */
void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
+
}
left=toe.left;
right=toe.right;
istuple=true;
- } else if (abstractexpr instanceof TupleOfExpr) {
+ } else if (abstractexpr instanceof ElementOfExpr) {
ElementOfExpr eoe=(ElementOfExpr) abstractexpr;
d=eoe.set;
left=eoe.element;
Rule r=(Rule)state.vRules.get(i);
if (r.getInclusion().getTargetDescriptors().contains(sd)) {
for(int j=0;j<mun.numUpdates();j++) {
- UpdateNode un=mun.getUpdate(i);
+ UpdateNode un=mun.getUpdate(j);
if (un.getRule()==r) {
/* Update for rule rule r */
String name=(String)rg.updatenames.get(un);
VarDescriptor right=VarDescriptor.makeNew("right");
if (u.getType()==Updates.ABSTRACT) {
generate_abstract(cr, removal, slot0, slot1, u, rg);
+ return;
}
switch(u.getType()) {
CLI_CLASS = CLI.class
OTHER_CLASS = State.class LineCount.class Symbol.class
-IR_CLASS = IR/ParseNode.class IR/ParseNodeVector.class IR/ParseNodeDOTVisitor.class \
-IR/SemanticChecker.class IR/Expr.class IR/VarExpr.class IR/OpExpr.class IR/DotExpr.class \
-IR/LiteralExpr.class IR/IntegerLiteralExpr.class IR/BooleanLiteralExpr.class \
-IR/TokenLiteralExpr.class IR/Descriptor.class IR/TypeDescriptor.class IR/StructureTypeDescriptor.class \
-IR/MissingTypeDescriptor.class IR/ReservedTypeDescriptor.class IR/ArrayDescriptor.class \
-IR/FieldDescriptor.class IR/LabelDescriptor.class IR/ReservedFieldDescriptor.class \
-IR/SymbolTable.class IR/IRException.class IR/Opcode.class IR/SimpleIRErrorReporter.class \
-IR/IRErrorReporter.class IR/SetDescriptor.class IR/MissingSetDescriptor.class \
-IR/RelationDescriptor.class IR/ReservedSetDescriptor.class IR/TokenSetDescriptor.class \
-IR/Quantifier.class IR/SetQuantifier.class IR/ImageSetExpr.class \
-IR/CastExpr.class IR/SizeofExpr.class IR/SetExpr.class IR/VarDescriptor.class \
-IR/LogicStatement.class IR/Predicate.class IR/InclusionPredicate.class \
-IR/ExprPredicate.class IR/Constraint.class IR/RelationExpr.class \
-IR/RelationQuantifier.class IR/ForQuantifier.class IR/GraphNode.class \
-IR/DependencyBuilder.class IR/RelationInclusion.class IR/SetInclusion.class \
-IR/TupleOfExpr.class IR/ElementOfExpr.class IR/Rule.class IR/Inclusion.class \
-IR/NaiveGenerator.class IR/CodeWriter.class IR/SymbolTableStack.class \
-IR/StandardCodeWriter.class IR/WorklistGenerator.class IR/WorkList.class \
-IR/Optimizer.class IR/MetaInclusion.class IR/SizeofFunction.class \
-IR/RelationFunctionExpr.class
-
-#MODEL_CLASS = Field.class Literal.class Quantifier.class \
-#Set.class TypeElement.class \
-#MDElementExpr.class Rule.class Guard.class Type.class \
-#ParseException.class ModelInclusionConstraint.class
+IR_CLASS = IR/ParseNode.class IR/ParseNodeVector.class \
+IR/ParseNodeDOTVisitor.class IR/SemanticChecker.class IR/Expr.class \
+IR/VarExpr.class IR/OpExpr.class IR/DotExpr.class IR/LiteralExpr.class \
+IR/IntegerLiteralExpr.class IR/BooleanLiteralExpr.class \
+IR/TokenLiteralExpr.class IR/Descriptor.class IR/TypeDescriptor.class \
+IR/StructureTypeDescriptor.class IR/MissingTypeDescriptor.class \
+IR/ReservedTypeDescriptor.class IR/ArrayDescriptor.class \
+IR/FieldDescriptor.class IR/LabelDescriptor.class \
+IR/ReservedFieldDescriptor.class IR/SymbolTable.class \
+IR/IRException.class IR/Opcode.class IR/SimpleIRErrorReporter.class \
+IR/IRErrorReporter.class IR/SetDescriptor.class \
+IR/MissingSetDescriptor.class IR/RelationDescriptor.class \
+IR/ReservedSetDescriptor.class IR/TokenSetDescriptor.class \
+IR/Quantifier.class IR/SetQuantifier.class IR/ImageSetExpr.class \
+IR/CastExpr.class IR/SizeofExpr.class IR/SetExpr.class \
+IR/VarDescriptor.class IR/LogicStatement.class IR/Predicate.class \
+IR/InclusionPredicate.class IR/ExprPredicate.class IR/Constraint.class \
+IR/RelationExpr.class IR/RelationQuantifier.class \
+IR/ForQuantifier.class IR/GraphNode.class IR/DependencyBuilder.class \
+IR/RelationInclusion.class IR/SetInclusion.class IR/TupleOfExpr.class \
+IR/ElementOfExpr.class IR/Rule.class IR/Inclusion.class \
+IR/NaiveGenerator.class IR/CodeWriter.class IR/SymbolTableStack.class \
+IR/StandardCodeWriter.class IR/WorklistGenerator.class \
+IR/WorkList.class IR/Optimizer.class IR/MetaInclusion.class \
+IR/SizeofFunction.class IR/RelationFunctionExpr.class \
+IR/RepairGenerator.class IR/AbstractInterferes.class \
+IR/PrettyPrinter.class IR/AbstractRepair.class IR/Quantifiers.class \
+IR/Binding.class IR/ConcreteInterferes.class IR/Conjunction.class \
+IR/Repair.class IR/ConsequenceNode.class IR/Cost.class \
+IR/DNFConstraint.class IR/DNFExpr.class IR/DNFPredicate.class \
+IR/RuleConjunction.class IR/DNFRule.class IR/ScopeNode.class \
+IR/SemanticAnalyzer.class IR/GraphAnalysis.class IR/SetAnalysis.class \
+IR/Sources.class IR/StructureGenerator.class IR/ImplicitSchema.class \
+IR/Termination.class IR/LinedMessage.class IR/TermNode.class \
+IR/UpdateNode.class IR/MultUpdateNode.class IR/Updates.class \
+IR/Walkable.class
+
+#MODEL_CLASS = Field.class Literal.class Quantifier.class Set.class \
+#TypeElement.class MDElementExpr.class Rule.class Guard.class \
+#Type.class ParseException.class ModelInclusionConstraint.class
ALL_CLASS = $(COMPILER_CLASS) $(CLI_CLASS) $(OTHER_CLASS) $(IR_CLASS)
rm $(SCANNER).lex.java
javadoc:
- javadoc -package -d ../javadoc/ -windowtitle MCC $(ALLJAVA)
+ javadoc -source 1.4 -classpath ../ -package -d ../javadoc/ -windowtitle MCC $(ALLJAVA)
projects / repair.git / commitdiff