constonode=new Hashtable();
nodetonode=new Hashtable();
constructnodes();
- constructconjunctionnodes();
- constructconjunctionedges();
}
+ public Set computeOrdering() {
+ HashSet allnodes=new HashSet();
+ allnodes.addAll(constnodes);
+ allnodes.addAll(nodes);
+ boolean acyclic=GraphNode.DFS.depthFirstSearch(allnodes);
+ if (!acyclic) {
+ throw new Error("Cylic dependency between constraints.");
+ }
+ TreeSet topologicalsort = new TreeSet(new Comparator() {
+ public boolean equals(Object obj) { return false; }
+ public int compare(Object o1, Object o2) {
+ GraphNode g1 = (GraphNode) o1;
+ GraphNode g2 = (GraphNode) o2;
+ return g1.getFinishingTime() - g2.getFinishingTime();
+ }
+ });
+
+ topologicalsort.addAll(constnodes);
+ return topologicalsort;
+ }
+
public void addNode(GraphNode gn) {
GraphNode gn2=new GraphNode(gn.getLabel(),gn.getTextLabel(),gn);
nodes.add(gn2);
}
public void associateWithConstraint(GraphNode gn, Constraint c) {
+ if (!nodetonode.containsKey(gn)) {
+ addNode(gn);
+ }
GraphNode ggn=(GraphNode)nodetonode.get(gn);
GraphNode gc=(GraphNode)constonode.get(c);
GraphNode.Edge e=new GraphNode.Edge("associated",ggn);
}
public void requiresConstraint(GraphNode gn, Constraint c) {
+ if (!nodetonode.containsKey(gn)) {
+ addNode(gn);
+ }
GraphNode ggn=(GraphNode)nodetonode.get(gn);
GraphNode gc=(GraphNode)constonode.get(c);
GraphNode.Edge e=new GraphNode.Edge("requires",gc);
ggn.addEdge(e);
}
+ public void traversedependences(Termination termination) {
+ constructconjunctionnodes(termination);
+ constructconjunctionedges(termination);
+ Set removedset=termination.removedset;
+
+ for(int i=0;i<state.vConstraints.size();i++) {
+ Constraint c=(Constraint)state.vConstraints.get(i);
+ Set conjset=(Set)termination.conjunctionmap.get(c);
+ HashSet exploredset=new HashSet();
+
+ for(Iterator it=conjset.iterator();it.hasNext();) {
+ GraphNode gn=(GraphNode)it.next();
+ recursedependence(c,termination,exploredset,gn);
+ }
+ }
+ }
+
+ void recursedependence(Constraint c,Termination termination, HashSet exploredset, GraphNode gn) {
+ Set removedset=termination.removedset;
+ Set conjunctionset=termination.conjunctions;
+
+ if (removedset.contains(gn))
+ return;
+ exploredset.add(gn);
+ associateWithConstraint(gn,c);
+ for(Iterator it=gn.edges();it.hasNext();) {
+ GraphNode.Edge e=(GraphNode.Edge) it.next();
+ GraphNode gn2=e.getTarget();
+ if (!(exploredset.contains(gn2)||
+ conjunctionset.contains(gn2)))
+ recursedependence(c,termination,exploredset,gn2);
+ }
+ }
+
/** Constructs a node for each Constraint */
private void constructnodes() {
for(int i=0;i<state.vConstraints.size();i++) {
}
}
- private void constructconjunctionnodes() {
- for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
- GraphNode conjnode=(GraphNode)it.next();
- TermNode tn=(TermNode)conjnode.getOwner();
- Conjunction conj=tn.getConjunction();
- addNode(conjnode);
- }
+ private void constructconjunctionnodes(Termination termination) {
+ /*for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+ GraphNode conjnode=(GraphNode)it.next();
+ TermNode tn=(TermNode)conjnode.getOwner();
+ Conjunction conj=tn.getConjunction();
+ addNode(conjnode);
+ }*/
+ Set removedset=termination.removedset;
+
for(int i=0;i<state.vConstraints.size();i++) {
Constraint c=(Constraint)state.vConstraints.get(i);
Set conjset=(Set)termination.conjunctionmap.get(c);
for(Iterator it=conjset.iterator();it.hasNext();) {
GraphNode gn=(GraphNode)it.next();
- associateWithConstraint(gn,c);
+ if (!removedset.contains(gn))
+ associateWithConstraint(gn,c);
}
}
}
- private void constructconjunctionedges() {
+ private void constructconjunctionedges(Termination termination) {
+ Set removedset=termination.removedset;
for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
GraphNode conjnode=(GraphNode)it.next();
+ if (removedset.contains(conjnode))
+ continue;
+
TermNode tn=(TermNode)conjnode.getOwner();
Conjunction conj=tn.getConjunction();
for(int i=0;i<conj.size();i++) {
continue;
for(Iterator fit=functions.iterator();fit.hasNext();) {
Function f=(Function)fit.next();
- if (rulesensurefunction(f))
+ if (rulesensurefunction(state,f,false))
continue; //no constraint needed to ensure
- Set s=providesfunction(f);
+ Set s=providesfunction(state,f);
if (s.size()==0) {
- System.out.println("Error: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
- System.exit(-1);
+ System.out.println("Warning: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
+ continue;
}
Constraint c=(Constraint)s.iterator().next(); //Take the first one
requiresConstraint(conjnode,c);
}
}
- private boolean rulesensurefunction(Function f) {
+ /** This method determines whether the model definition rules
+ * ensure that the relation and evaluation domain descriped by f
+ * is either a function (if isPartial=false) or a partial function
+ * (if isPartial=true). */
+
+ static private boolean rulesensurefunction(State state,Function f, boolean isPartial) {
boolean foundrule=false;
for(int i=0;i<state.vRules.size();i++) {
Rule r=(Rule)state.vRules.get(i);
RelationInclusion ri=(RelationInclusion)r.getInclusion();
Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
SetDescriptor sd=e.getSet();
- if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
+ if (sd==null)
+ return false;
+ if (state.setanalysis.noIntersection(f.getSet(),sd))
continue; /* This rule doesn't effect the function */
if (foundrule) /* two different rules are a problem */
return false;
SetQuantifier sq=(SetQuantifier)q;
if (ve.getVar()!=sq.getVar())
return false;
- if (!sq.getSet().isSubset(f.getSet()))
- return false;
- if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
- ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
- return false;
+ if (!isPartial) {
+ if (!sq.getSet().isSubset(f.getSet()))
+ return false;
+ if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+ ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
+ return false;
+ }
Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
- if (e2.isSafe())
+ if (isPartial||e2.isSafe())
foundrule=true;
else
return false;
return foundrule;
}
- private Set providesfunction(Function f) {
+ static private Set providesfunction(State state, Function f) {
HashSet set=new HashSet();
for(int i=0;i<state.vConstraints.size();i++) {
Constraint c=(Constraint)state.vConstraints.get(i);
return set;
}
+
+ /** This method determines whether the model definition rules
+ * ensure that the relation r (or inverse relation if inverse is
+ * true) evaluated on the domain sd is either a function (if
+ * isPartial=false) or a partial function (if isPartial=true). */
+
+ static public boolean rulesensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse, boolean isPartial) {
+ return rulesensurefunction(state, new Function(r,sd,inverse,null),isPartial);
+ }
+
+ /** This method determines whether the model constraints ensure
+ * that the relation r (or inverse relation if inverse is true)
+ * evaluated on the domain sd is either a function (if
+ * isPartial=false) or a partial function (if isPartial=true). */
+
+ static public boolean constraintsensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse) {
+ Set constraints=providesfunction(state, new Function(r,sd,inverse,null));
+ return (!constraints.isEmpty());
+ }
+
public static class Function {
private RelationDescriptor rd;
private SetDescriptor sd;
private boolean inverse;
+ private Expr expr;
- public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse) {
+ public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse,Expr e) {
this.inverse=inverse;
this.sd=sd;
this.rd=r;
+ this.expr=e;
+ }
+
+ public Expr getExpr() {
+ return expr;
}
public SetDescriptor getSet() {
projects / repair.git / blobdiff