X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=cyclegraph.cc;h=def51f9671e346251a4f108abe1c78c8d09a8bfe;hp=77c0b68f13cfa86ef88ac0274b20435feec6c637;hb=6014243b7130f34b7ffd1098da225b0b8de5c328;hpb=4fa31aac91303266f4c87a6cd5d60cbab34135db

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 77c0b68..def51f9 100644
--- 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. */
@@ -314,12 +313,12 @@ static void print_node(FILE *file, const CycleNode *node, int label)
 {
 	if (node->is_promise()) {
 		const Promise *promise = node->getPromise();
-		int idx = model->get_promise_number(promise);
+		int idx = promise->get_index();
 		fprintf(file, "P%u", idx);
 		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);