cyclegraph: add documentation

[model-checker.git] / cyclegraph.cc

diff --git a/cyclegraph.cc b/cyclegraph.cc
index e3d0d8366694d53c44170ba589062df01d179aa0..8326f28b7ee3a2c3be6332fc383f959707040eac 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -62,14 +62,8 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
        CycleNode *fromnode = getNode(from);
        CycleNode *tonode = getNode(to);
 
-       if (!hasCycles) {
-               // Reflexive edges are cycles
-               hasCycles = (from == to);
-       }
-       if (!hasCycles) {
-               // Check for Cycles
+       if (!hasCycles)
                hasCycles = checkReachable(tonode, fromnode);
-       }
 
        if (fromnode->addEdge(tonode))
                rollbackvector.push_back(fromnode);
@@ -86,10 +80,8 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
         * for the possibility of sending to's write value to rmwnode
         */
        if (rmwnode != NULL && !to->is_rmw()) {
-               if (!hasCycles) {
-                       // Check for Cycles
+               if (!hasCycles)
                        hasCycles = checkReachable(tonode, rmwnode);
-               }
 
                if (rmwnode->addEdge(tonode))
                        rollbackvector.push_back(rmwnode);
@@ -131,16 +123,9 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
                }
        }
 
-
-       if (!hasCycles) {
-               // Reflexive edges are cycles
-               hasCycles = (from == rmw);
-       }
-       if (!hasCycles) {
-               // With promises we could be setting up a cycle here if we aren't
-               // careful...avoid it..
+       if (!hasCycles)
                hasCycles = checkReachable(rmwnode, fromnode);
-       }
+
        if (fromnode->addEdge(rmwnode))
                rollbackvector.push_back(fromnode);
 }
@@ -332,6 +317,7 @@ unsigned int CycleNode::getNumBackEdges() const
 /**
  * Adds an edge from this CycleNode to another CycleNode.
  * @param node The node to which we add a directed edge
+ * @return True if this edge is a new edge; false otherwise
  */
 bool CycleNode::addEdge(CycleNode *node)
 {