X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=c76a28972bf4e6f9fac715386a0a69cb1f4956e3;hb=8cb0f16c5f8bed452509785b9d8c18133a38e27d;hp=97a898926e49dfd8480412c67a2900dfd8db5f15;hpb=7372f39c67d6e4ea2dc142fca9c1b61c590af94c;p=model-checker.git

diff --git a/model.h b/model.h
index 97a8989..c76a289 100644
--- a/model.h
+++ b/model.h
@@ -108,7 +108,7 @@ public:
 	void add_thread(Thread *t);
 	void remove_thread(Thread *t);
 	Thread * get_thread(thread_id_t tid) const;
-	Thread * get_thread(ModelAction *act) const;
+	Thread * get_thread(const ModelAction *act) const;
 
 	bool is_enabled(Thread *t) const;
 	bool is_enabled(thread_id_t tid) const;
@@ -121,7 +121,7 @@ public:
 	ClockVector * get_cv(thread_id_t tid) const;
 	ModelAction * get_parent_action(thread_id_t tid) const;
 	void check_promises_thread_disabled();
-	void mo_check_promises(thread_id_t tid, const ModelAction *write);
+	void mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction * read);
 	void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
 	bool isfeasibleprefix() const;
 
@@ -257,7 +257,6 @@ private:
 
 	void print_infeasibility(const char *prefix) const;
 	bool is_feasible_prefix_ignore_relseq() const;
-	bool is_infeasible_ignoreRMW() const;
 	bool is_infeasible() const;
 	bool is_deadlocked() const;
 	bool is_complete_execution() const;