nodestack: bugfix - rewrite 'may-read-from' and 'future values' as the same set

[model-checker.git] / cyclegraph.cc

diff --git a/cyclegraph.cc b/cyclegraph.cc
index e0b221514f9bd88b0785839b44e2436921f9f4b8..1dbb12d9d25e2179895554817133b1c0267f179d 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -3,6 +3,7 @@
 #include "common.h"
 #include "promise.h"
 #include "model.h"
+#include "threads-model.h"
 
 /** Initializes a CycleGraph object. */
 CycleGraph::CycleGraph() :
@@ -38,8 +39,7 @@ void CycleGraph::putNode(const ModelAction *act, CycleNode *node)
  */
 void CycleGraph::putNode(const Promise *promise, CycleNode *node)
 {
-       const ModelAction *reader = promise->get_action();
-       readerToPromiseNode.put(reader, node);
+       promiseToNode.put(promise, node);
 #if SUPPORT_MOD_ORDER_DUMP
        nodeList.push_back(node);
 #endif
@@ -51,8 +51,7 @@ void CycleGraph::putNode(const Promise *promise, CycleNode *node)
  */
 void CycleGraph::erasePromiseNode(const Promise *promise)
 {
-       const ModelAction *reader = promise->get_action();
-       readerToPromiseNode.put(reader, NULL);
+       promiseToNode.put(promise, NULL);
 #if SUPPORT_MOD_ORDER_DUMP
        /* Remove the promise node from nodeList */
        CycleNode *node = getNode_noCreate(promise);
@@ -73,7 +72,7 @@ CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
 /** @return The corresponding CycleNode, if exists; otherwise NULL */
 CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const
 {
-       return readerToPromiseNode.get(promise->get_action());
+       return promiseToNode.get(promise);
 }
 
 /**
@@ -116,10 +115,10 @@ CycleNode * CycleGraph::getNode(const Promise *promise)
 /**
  * @return false if the resolution results in a cycle; true otherwise
  */
-bool CycleGraph::resolvePromise(ModelAction *reader, ModelAction *writer,
+bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer,
                promise_list_t *mustResolve)
 {
-       CycleNode *promise_node = readerToPromiseNode.get(reader);
+       CycleNode *promise_node = promiseToNode.get(promise);
        CycleNode *w_node = actionToNode.get(writer);
        ASSERT(promise_node);
 
@@ -308,10 +307,11 @@ bool CycleGraph::addEdge(const T *from, const U *to)
 
        return addNodeEdge(fromnode, tonode);
 }
-/* Instantiate three forms of CycleGraph::addEdge */
+/* Instantiate four forms of CycleGraph::addEdge */
 template bool CycleGraph::addEdge(const ModelAction *from, const ModelAction *to);
 template bool CycleGraph::addEdge(const ModelAction *from, const Promise *to);
 template bool CycleGraph::addEdge(const Promise *from, const ModelAction *to);
+template bool CycleGraph::addEdge(const Promise *from, const Promise *to);
 
 #if SUPPORT_MOD_ORDER_DUMP
 
@@ -405,13 +405,13 @@ bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) cons
 }
 
 /**
- * Checks whether one ModelAction can reach another ModelAction/Promise
- * @param from The ModelAction from which to begin exploration
+ * Checks whether one ModelAction/Promise can reach another ModelAction/Promise
+ * @param from The ModelAction or Promise from which to begin exploration
  * @param to The ModelAction or Promise to reach
  * @return True, @a from can reach @a to; otherwise, false
  */
-template <typename T>
-bool CycleGraph::checkReachable(const ModelAction *from, const T *to) const
+template <typename T, typename U>
+bool CycleGraph::checkReachable(const T *from, const U *to) const
 {
        CycleNode *fromnode = getNode_noCreate(from);
        CycleNode *tonode = getNode_noCreate(to);
@@ -421,11 +421,13 @@ bool CycleGraph::checkReachable(const ModelAction *from, const T *to) const
 
        return checkReachable(fromnode, tonode);
 }
-/* Instantiate two forms of CycleGraph::checkReachable */
+/* Instantiate three forms of CycleGraph::checkReachable */
 template bool CycleGraph::checkReachable(const ModelAction *from,
                const ModelAction *to) const;
 template bool CycleGraph::checkReachable(const ModelAction *from,
                const Promise *to) const;
+template bool CycleGraph::checkReachable(const Promise *from,
+               const ModelAction *to) const;
 
 /** @return True, if the promise has failed; false otherwise */
 bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
@@ -440,6 +442,8 @@ bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) cons
                CycleNode *node = queue.back();
                queue.pop_back();
 
+               if (node->getPromise() == promise)
+                       return true;
                if (!node->is_promise() &&
                                promise->eliminate_thread(node->getAction()->get_tid()))
                        return true;