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 7fadcbda00d8b6f02f9cfe81d5cd3f423e9a3a2b..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);
 
@@ -443,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;