X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=cyclegraph.cc;h=967b0763abbdcdba0ec35cdd2608cb0fa94caa13;hb=50b95c3747f4fe79b2ab1a1a6fc303224e16e418;hp=1eb1add33fc255e4f53e9044b3d3850b422668dd;hpb=3519c47202090f3c4a69de0e89aaa2617b17ff75;p=model-checker.git

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 1eb1add..967b076 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -3,7 +3,8 @@
 
 /** Initializes a CycleGraph object. */
 CycleGraph::CycleGraph() :
-	hasCycles(false)
+	hasCycles(false),
+	oldCycles(false)
 {
 }
 
@@ -31,7 +32,7 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) {
  * @param to The edge points to this ModelAction
  * @param from The edge comes from this ModelAction
  */
-void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
+void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
 	CycleNode *fromnode=getNode(from);
 	CycleNode *tonode=getNode(to);
 
@@ -39,6 +40,8 @@ void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
 		// Check for Cycles
 		hasCycles=checkReachable(tonode, fromnode);
 	}
+
+	rollbackvector.push_back(fromnode);
 	fromnode->addEdge(tonode);
 
 	CycleNode * rmwnode=fromnode->getRMW();
@@ -51,6 +54,7 @@ void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
 			// Check for Cycles
 			hasCycles=checkReachable(tonode, rmwnode);
 		}
+		rollbackvector.push_back(rmwnode);
 		rmwnode->addEdge(tonode);
 	}
 }
@@ -60,13 +64,15 @@ void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
  *  can occur in between the rmw and the from action.  Only one RMW
  *  action can read from a given write.
  */
-void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction *from) {
+void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 	CycleNode *fromnode=getNode(from);
 	CycleNode *rmwnode=getNode(rmw);
 
 	/* Two RMW actions cannot read from the same write. */
 	if (fromnode->setRMW(rmwnode)) {
 		hasCycles=true;
+	} else {
+		rmwrollbackvector.push_back(fromnode);
 	}
 
 	/* Transfer all outgoing edges from the from node to the rmw node */
@@ -75,12 +81,28 @@ void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction *from) {
 	std::vector<CycleNode *> * edges=fromnode->getEdges();
 	for(unsigned int i=0;i<edges->size();i++) {
 		CycleNode * tonode=(*edges)[i];
+		rollbackvector.push_back(rmwnode);
 		rmwnode->addEdge(tonode);
 	}
-
+	rollbackvector.push_back(fromnode);
 	fromnode->addEdge(rmwnode);
 }
 
+/**
+ * Checks whether one ModelAction can reach another.
+ * @param from The ModelAction from which to begin exploration
+ * @param to The ModelAction to reach
+ * @return True, @a from can reach @a to; otherwise, false
+ */
+bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) {
+	CycleNode *fromnode = actionToNode.get(from);
+	CycleNode *tonode = actionToNode.get(to);
+
+	if (!fromnode || !tonode)
+		return false;
+
+	return checkReachable(fromnode, tonode);
+}
 
 /**
  * Checks whether one CycleNode can reach another.
@@ -111,6 +133,28 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
 	return false;
 }
 
+/** Commit changes to the cyclegraph. */
+void CycleGraph::commitChanges() {
+	rollbackvector.resize(0);
+	rmwrollbackvector.resize(0);
+	oldCycles=hasCycles;
+}
+
+/** Rollback changes to the previous commit. */
+void CycleGraph::rollbackChanges() {
+	for (unsigned int i = 0; i < rollbackvector.size(); i++) {
+		rollbackvector[i]->popEdge();
+	}
+
+	for (unsigned int i = 0; i < rmwrollbackvector.size(); i++) {
+		rmwrollbackvector[i]->clearRMW();
+	}
+
+	hasCycles = oldCycles;
+	rollbackvector.resize(0);
+	rmwrollbackvector.resize(0);
+}
+
 /** @returns whether a CycleGraph contains cycles. */
 bool CycleGraph::checkForCycles() {
 	return hasCycles;
@@ -151,7 +195,8 @@ CycleNode * CycleNode::getRMW() {
  * @see CycleGraph::addRMWEdge
  */
 bool CycleNode::setRMW(CycleNode *node) {
-	CycleNode * oldhasRMW=hasRMW;
+	if (hasRMW!=NULL)
+		return true;
 	hasRMW=node;
-	return (oldhasRMW!=NULL);
+	return false;
 }