X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.cc;h=2dc2eae9503a92f1117be1345441242d3a8f1437;hb=bd6db524d36605b8eae0159f943b7e9e9361d7a5;hp=ec0ce45f55ae65ae77325889b0aa0bfe84444cf8;hpb=76bf58915289cb923cc95e237b64151bf799167c;p=model-checker.git

diff --git a/cyclegraph.cc b/cyclegraph.cc
index ec0ce45..2dc2eae 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -63,7 +63,7 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
 	CycleNode *tonode = getNode(to);
 
 	if (!hasCycles)
-		hasCycles = edgeCreatesCycle(fromnode, tonode);
+		hasCycles = checkReachable(tonode, fromnode);
 
 	if (fromnode->addEdge(tonode))
 		rollbackvector.push_back(fromnode);
@@ -81,7 +81,7 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
 	 */
 	if (rmwnode != NULL && !to->is_rmw()) {
 		if (!hasCycles)
-			hasCycles = edgeCreatesCycle(rmwnode, tonode);
+			hasCycles = checkReachable(tonode, rmwnode);
 
 		if (rmwnode->addEdge(tonode))
 			rollbackvector.push_back(rmwnode);
@@ -124,7 +124,7 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
 	}
 
 	if (!hasCycles)
-		hasCycles = edgeCreatesCycle(fromnode, rmwnode);
+		hasCycles = checkReachable(rmwnode, fromnode);
 
 	if (fromnode->addEdge(rmwnode))
 		rollbackvector.push_back(fromnode);
@@ -160,18 +160,6 @@ void CycleGraph::dumpGraphToFile(const char *filename) const
 }
 #endif
 
-/**
- * Checks whether the addition of an edge between these two nodes would create
- * a cycle in the graph.
- * @param from The CycleNode from which the edge would start
- * @param to The CycleNode to which the edge would point
- * @return True if this edge would create a cycle; false otherwise
- */
-bool CycleGraph::edgeCreatesCycle(const CycleNode *from, const CycleNode *to) const
-{
-	return (from == to) || checkReachable(to, from);
-}
-
 /**
  * Checks whether one ModelAction can reach another.
  * @param from The ModelAction from which to begin exploration