Bug fix for broken treatment of promises + coherence based pruning to regain pruning...

[model-checker.git] / cyclegraph.cc

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 0ec95b057bec48bce7d914e316066c2c62de065c..def51f9671e346251a4f108abe1c78c8d09a8bfe 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -2,7 +2,6 @@
 #include "action.h"
 #include "common.h"
 #include "promise.h"
-#include "model.h"
 #include "threads-model.h"
 
 /** Initializes a CycleGraph object. */
@@ -319,7 +318,7 @@ static void print_node(FILE *file, const CycleNode *node, int label)
                if (label) {
                        int first = 1;
                        fprintf(file, " [label=\"P%d, T", idx);
-                       for (unsigned int i = 0 ; i < model->get_num_threads(); i++)
+                       for (unsigned int i = 0 ; i < promise->max_available_thread_idx(); i++)
                                if (promise->thread_is_available(int_to_id(i))) {
                                        fprintf(file, "%s%u", first ? "": ",", i);
                                        first = 0;
@@ -457,9 +456,8 @@ bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) cons
 
                if (node->getPromise() == promise)
                        return true;
-               if (!node->is_promise() &&
-                               promise->eliminate_thread(node->getAction()->get_tid()))
-                       return true;
+               if (!node->is_promise())
+                       promise->eliminate_thread(node->getAction()->get_tid());
 
                for (unsigned int i = 0; i < node->getNumEdges(); i++) {
                        CycleNode *next = node->getEdge(i);