From: Brian Norris <banorris@uci.edu>
Date: Fri, 17 Aug 2012 00:06:31 +0000 (-0700)
Subject: cyclegraph: add public CycleGraph::checkReachable()
X-Git-Tag: pldi2013~261
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=d3f14b49a90dc60f1976529f3cd784832c1fad32

cyclegraph: add public CycleGraph::checkReachable()

The private CycleGraph::checkReachable() function can be useful externally,
when provided with two ModelActions. This implements a small wrapper for public
usage.
---

diff --git a/cyclegraph.cc b/cyclegraph.cc
index b140ded..3168923 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -81,6 +81,21 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 	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.
diff --git a/cyclegraph.h b/cyclegraph.h
index c8ba531..2e523d7 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -21,6 +21,8 @@ class CycleGraph {
 	bool checkForCycles();
 	void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
 
+	bool checkReachable(const ModelAction *from, const ModelAction *to);
+
  private:
 	CycleNode * getNode(const ModelAction *);