* files.
*
* @author le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.14 2005/02/20 20:31:28 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.15 2005/09/30 06:18:11 bdemsky Exp $</tt>
*/
public class CLI {
/**
System.out.println("-time");
System.out.println("-omitcomp");
System.out.println("-mergenodes");
+ System.out.println("-debuggraph");
System.exit(-1);
}
Compiler.REPAIR=false;
} else if (args[i].equals("-omitcomp")) {
Compiler.OMITCOMP=true;
+ } else if (args[i].equals("-debuggraph")) {
+ Compiler.DEBUGGRAPH=true;
} else if (args[i].equals("-mergenodes")) {
Compiler.MERGENODES=true;
} else if (args[i].equals("-depth")) {
public static boolean OMITCOMP=false;
public static boolean MERGENODES=false;
public static boolean TIME=false;
+ public static boolean DEBUGGRAPH=false;
public static Vector debuggraphs=new Vector();
nodes.addAll(state.rulenodes.values());
FileOutputStream dotfile;
- dotfile = new FileOutputStream(cli.infile + ".dependencies.edgelabels.dot");
- GraphNode.useEdgeLabels = true;
- GraphNode.DOTVisitor.visit(dotfile, nodes);
- dotfile.close();
dotfile = new FileOutputStream(cli.infile + ".dependencies.dot");
- GraphNode.useEdgeLabels = false;
GraphNode.DOTVisitor.visit(dotfile, nodes);
dotfile.close();
} catch (Exception e) {
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();
import java.util.*;
import java.io.*;
+import MCC.Compiler;
public class GraphNode {
- public static boolean useEdgeLabels;
-
/* NodeStatus enumeration pattern ***********/
-
+
public static final NodeStatus UNVISITED = new NodeStatus("UNVISITED");
public static final NodeStatus PROCESSING = new NodeStatus("PROCESSING");
public static final NodeStatus FINISHED = new NodeStatus("FINISHED");
/* Edge *****************/
public static class Edge {
-
+
private String label;
private GraphNode target;
private GraphNode source;
int discoverytime = -1;
int finishingtime = -1; /* used for searches */
- Vector edges = new Vector();
+ Vector edges = new Vector();
Vector inedges = new Vector();
String nodelabel;
String textlabel;
- NodeStatus status = UNVISITED;
+ NodeStatus status = UNVISITED;
String dotnodeparams = new String();
Object owner = null;
boolean merge=false;
dotnodeparams = new String();
}
}
-
+
public void setStatus(NodeStatus status) {
if (status == null) {
throw new NullPointerException();
public String getTextLabel() {
return textlabel;
}
-
+
public NodeStatus getStatus() {
return this.status;
}
public static class DOTVisitor {
-
+
java.io.PrintWriter output;
int tokennumber;
int color;
-
+
private DOTVisitor(java.io.OutputStream output) {
tokennumber = 0;
color = 0;
this.output = new java.io.PrintWriter(output, true);
}
-
+
private String getNewID(String name) {
tokennumber = tokennumber + 1;
return new String (name+tokennumber);
Collection nodes;
Collection special;
-
+
public static void visit(java.io.OutputStream output, Collection nodes) {
visit(output,nodes,null);
}
visitor.nodes = nodes;
visitor.make();
}
-
+
private void make() {
output.println("digraph dotvisitor {");
output.println("\trotate=90;");
traverse();
output.println("}\n");
}
-
- private void traverse() {
+
+ private void traverse() {
Set cycleset=GraphNode.findcycles(nodes);
Iterator i = nodes.iterator();
if (nodes.contains(node)) {
for(Iterator nodeit=nonmerge(node).iterator();nodeit.hasNext();) {
GraphNode node2=(GraphNode)nodeit.next();
- String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
+ String edgelabel = Compiler.DEBUGGRAPH ? "label=\"" + edge.getLabel() + "\"" : "label=\"\"";
output.println("\t" + gn.getLabel() + " -> " + node2.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];");
}
}
}
- /** This function returns the set of nodes involved in cycles.
+ /** This function returns the set of nodes involved in cycles.
* It only considers cycles containing nodes in the set 'nodes'.
*/
public static Set findcycles(Collection nodes) {
}
/**
- * DFS encapsulates the depth first search algorithm
+ * DFS encapsulates the depth first search algorithm
*/
public static class DFS {
HashMap sccmap;
HashMap sccmaprev;
- private DFS(Collection nodes) {
+ private DFS(Collection nodes) {
this.nodes = nodes;
}
/** Calculates the strong connected components for the graph composed
if (nodes == null) {
throw new NullPointerException();
}
-
+
DFS dfs = new DFS(nodes);
return dfs.go();
}
- private boolean go() {
+ private boolean go() {
Iterator i;
time = 0;
boolean acyclic=true;
i = nodes.iterator();
while (i.hasNext()) {
GraphNode gn = (GraphNode) i.next();
- gn.reset();
- }
+ gn.reset();
+ }
i = nodes.iterator();
while (i.hasNext()) {
GraphNode gn = (GraphNode) i.next();
- assert gn.getStatus() != PROCESSING;
+ assert gn.getStatus() != PROCESSING;
if (gn.getStatus() == UNVISITED) {
if (!dfs(gn))
acyclic=false;
- }
+ }
}
return acyclic;
}
}
}
-
private void name_updates() {
int count=0;
for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
dCurrentType = type;
// parse the labels and fields
- if (!parse_labelsandfields(pn.getChild("lf"))) {
+ if (pn.getChild("lf")!=null && !parse_labelsandfields(pn.getChild("lf"))) {
ok = false;
}
generateconjunctionnodes();
constraintdependence=new ConstraintDependence(state,this);
- debugmsg("Generating scope nodes");
+ debugmsg("*****Generating scope nodes*****");
generatescopenodes();
- debugmsg("Generating repair nodes");
+ debugmsg("*****Generating repair nodes*****");
generaterepairnodes();
- debugmsg("Generating data structure nodes");
+ debugmsg("*****Generating data structure nodes*****");
generatedatastructureupdatenodes();
- debugmsg("Generating compensation nodes");
+ debugmsg("*****Generating compensation nodes*****");
if (!Compiler.OMITCOMP)
generatecompensationnodes();
- debugmsg("Generating abstract edges");
+ debugmsg("*****Generating abstract edges*****");
generateabstractedges();
- debugmsg("Generating scope edges");
+ debugmsg("*****Generating scope edges*****");
generatescopeedges();
- debugmsg("Generating update edges");
+ debugmsg("*****Generating update edges*****");
generateupdateedges();
TupleOfExpr toe=(TupleOfExpr)e;
if (negated) {
GraphNode agn=(GraphNode)abstractremove.get(toe.relation);
- GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge edge=new GraphNode.Edge("requirestupleremove",agn);
gn.addEdge(edge);
} else {
GraphNode agn=(GraphNode)abstractadd.get(toe.relation);
- GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge edge=new GraphNode.Edge("requirestupleadd",agn);
gn.addEdge(edge);
}
} else if (e instanceof ElementOfExpr) {
ElementOfExpr eoe=(ElementOfExpr)e;
if (negated) {
GraphNode agn=(GraphNode)abstractremove.get(eoe.set);
- GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge edge=new GraphNode.Edge("requireselementremove",agn);
gn.addEdge(edge);
} else {
GraphNode agn=(GraphNode)abstractadd.get(eoe.set);
- GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge edge=new GraphNode.Edge("requireselementadd",agn);
gn.addEdge(edge);
}
} else throw new Error("Unrecognized Abstract Update");
/* Cycle through the rules to look for possible conflicts */
for(int i=0;i<state.vRules.size();i++) {
Rule r=(Rule) state.vRules.get(i);
+ if (Compiler.DEBUGGRAPH) {
+ System.out.println(gn.getLabel()+"--->"+((GraphNode)scopesatisfy.get(r)).getLabel());
+ }
if (concreteinterferes.interferes(mun,r,true)) {
GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
- GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+ GraphNode.Edge e=new GraphNode.Edge("satisfyscopeinterferes",scopenode);
gn.addEdge(e);
}
+ if (Compiler.DEBUGGRAPH) {
+ System.out.println(gn.getLabel()+"--->"+((GraphNode)scopefalsify.get(r)).getLabel());
+ }
if (concreteinterferes.interferes(mun,r,false)) {
GraphNode scopenode=(GraphNode)scopefalsify.get(r);
- GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+ GraphNode.Edge e=new GraphNode.Edge("falsifyscopeinterferes",scopenode);
gn.addEdge(e);
}
}
if (abstractinterferes.checkrelationconstraint(ar, cons))
continue;
if (AbstractInterferes.interferesquantifier(ar,cons)) {
- GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ GraphNode.Edge e=new GraphNode.Edge("interferesquantifier",gn2);
gn.addEdge(e);
} else {
for(int i=0;i<conj.size();i++) {
continue;
if (getConstraint(gn)==null||
!abstractinterferes.interferemodifies(ar,getConstraint(gn),dp,cons)) {
- GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ GraphNode.Edge e=new GraphNode.Edge("interferesmodify",gn2);
gn.addEdge(e);
break;
}
TermNode tn2=(TermNode)gn2.getOwner();
ScopeNode sn2=tn2.getScope();
if (AbstractInterferes.interfereswithrule(ar,sn2.getRule(),sn2.getSatisfy())) {
- GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ GraphNode.Edge e=new GraphNode.Edge("interfereswithrule",gn2);
gn.addEdge(e);
}
}
DNFPredicate dp=conj.get(i);
if (abstractinterferes.scopeinterfereswithpredicate(sn,dp)||
AbstractInterferes.interfereswithquantifier(sn.getDescriptor(),sn.getSatisfy(),constr)) {
- GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
+ GraphNode.Edge e=new GraphNode.Edge("interferesconjunction",gn2);
GraphNode gnconseq=(GraphNode)consequence.get(sn);
gnconseq.addEdge(e);
break;
Rule r=(Rule) state.vRules.get(i);
if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
- GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+ GraphNode.Edge e=new GraphNode.Edge("interferesscopesatisfy2",scopenode);
GraphNode gnconseq=(GraphNode)consequence.get(sn);
gnconseq.addEdge(e);
}
if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
GraphNode scopenode=(GraphNode)scopefalsify.get(r);
- GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
+ GraphNode.Edge e=new GraphNode.Edge("interferesscopefalsify2",scopenode);
GraphNode gnconseq=(GraphNode)consequence.get(sn);
gnconseq.addEdge(e);
}
// GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),dp.name()+" "+ar.type(),tn2);
gn2.setOption(absrepoption);
- GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
+ GraphNode.Edge e=new GraphNode.Edge("abstractedge1",gn2);
gn.addEdge(e);
if (!predtoabstractmap.containsKey(dp))
predtoabstractmap.put(dp,new HashSet());
un.addUpdate(u);
if (abstractremove.containsKey(rq.relation)) {
GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
- GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge e=new GraphNode.Edge("requiresremove1",agn);
gn2.addEdge(e);
} else {
continue; /* Abstract repair doesn't exist */
un.addUpdate(u);
if (abstractremove.containsKey(sq.set)) {
GraphNode agn=(GraphNode)abstractremove.get(sq.set);
- GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge e=new GraphNode.Edge("requiresremove2",agn);
gn2.addEdge(e);
} else {
continue; /* Abstract repair doesn't exist */
continue;
mun.addUpdate(un);
- GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
+ GraphNode.Edge e=new GraphNode.Edge("abstractcomp"+compensationcount,gn2);
compensationcount++;
gn.addEdge(e);
updatenodes.add(gn2);
un.addUpdate(u);
if (abstractremove.containsKey(rq.relation)) {
GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
- GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge e=new GraphNode.Edge("requiresremove3",agn);
gn2.addEdge(e);
} else {
goodflag=false;break; /* Abstract repair doesn't exist */
un.addUpdate(u);
if (abstractremove.containsKey(sq.set)) {
GraphNode agn=(GraphNode)abstractremove.get(sq.set);
- GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge e=new GraphNode.Edge("requiresremove4",agn);
gn2.addEdge(e);
} else {
goodflag=false;break; /* Abstract repair doesn't exist */
mun.addUpdate(un);
}
if (goodflag) {
- GraphNode.Edge e=new GraphNode.Edge("abstract"+(removefromcount++),gn2);
+ GraphNode.Edge e=new GraphNode.Edge("abstract3"+(removefromcount++),gn2);
gn.addEdge(e);
updatenodes.add(gn2);
}
mun.addUpdate(un);
}
if (goodflag) {
- GraphNode.Edge e=new GraphNode.Edge("abstract"+modifycount,gn2);
+ GraphNode.Edge e=new GraphNode.Edge("abstract4"+modifycount,gn2);
modifycount++;
gn.addEdge(e);
updatenodes.add(gn2);
un.checkupdates()&&
debugmsg("Updates checked")) {
mun.addUpdate(un);
- GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
+ GraphNode.Edge e=new GraphNode.Edge("abstract5"+addtocount,gn2);
addtocount++;
gn.addEdge(e);
updatenodes.add(gn2);
un.addUpdate(u);
if (abstractadd.containsKey(rq.relation)) {
GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
- GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge e=new GraphNode.Edge("requiresadd5",agn);
gn.addEdge(e);
} else {
return false;
un.addUpdate(u);
if (abstractadd.containsKey(sq.set)) {
GraphNode agn=(GraphNode)abstractadd.get(sq.set);
- GraphNode.Edge e=new GraphNode.Edge("requires",agn);
+ GraphNode.Edge e=new GraphNode.Edge("requiresadd6",agn);
gn.addEdge(e);
} else {
return false;
structure.addChild(lf);
RESULT = structure;
:}
+ |
+ STRUCTURE ID:typename optsubtype:subtype OPENBRACE CLOSEBRACE
+ {:
+ debugMessage(PRODSTRING);
+ ParseNode structure = new ParseNode("structure", parser.curLine(6));
+ structure.addChild("name", parser.curLine(5)).addChild(typename);
+ if (subtype != null) {
+ structure.addChild(subtype);
+ }
+ RESULT = structure;
+ :}
| ID:type MULT ID:name SEMICOLON
{:
projects / repair.git / commitdiff