From: Brian Norris <banorris@uci.edu>
Date: Wed, 14 Nov 2012 23:55:59 +0000 (-0800)
Subject: model/promise: use ModelChecker is_enabled() interface
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=365a6079a1b43cbc0fce6299449a4ec62876fb20;p=cdsspec-compiler.git

model/promise: use ModelChecker is_enabled() interface

class Promise should not need to access Scheduler directly. Use the
ModelChecker interface.
---

diff --git a/model.cc b/model.cc
index daf2d15..3f200ed 100644
--- a/model.cc
+++ b/model.cc
@@ -1557,7 +1557,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
 		ModelAction *last = get_last_action(int_to_id(i));
 		Thread *th = get_thread(int_to_id(i));
 		if ((last && rf->happens_before(last)) ||
-				!scheduler->is_enabled(th) ||
+				!is_enabled(th) ||
 				th->is_complete())
 			future_ordered = true;
 
diff --git a/promise.cc b/promise.cc
index 68290ee..90591eb 100644
--- a/promise.cc
+++ b/promise.cc
@@ -11,11 +11,10 @@ bool Promise::increment_threads(thread_id_t tid) {
 		return false;
 	
 	synced_thread[id]=true;
-	enabled_type_t * enabled=model->get_scheduler()->get_enabled();
 	unsigned int sync_size=synced_thread.size();
 	int promise_tid=id_to_int(read->get_tid());
 	for(unsigned int i=1;i<model->get_num_threads();i++) {
-		if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && (enabled[i] != THREAD_DISABLED)) {
+		if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && model->is_enabled(int_to_id(i))) {
 			return false;
 		}
 	}
@@ -23,10 +22,9 @@ bool Promise::increment_threads(thread_id_t tid) {
 }
 
 bool Promise::check_promise() {
-	enabled_type_t * enabled=model->get_scheduler()->get_enabled();
 	unsigned int sync_size=synced_thread.size();
 	for(unsigned int i=1;i<model->get_num_threads();i++) {
-		if ((i >= sync_size || !synced_thread[i]) && (enabled[i] != THREAD_DISABLED)) {
+		if ((i >= sync_size || !synced_thread[i]) && model->is_enabled(int_to_id(i))) {
 			return false;
 		}
 	}