X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=5a127b1dd979a59c6d9cfe1e830ce0db7c58f860;hb=24dbae977ee0610d314b52a42a77f1a6f39752b3;hp=4fd2667753f4b3ae85698c6422921a1cf18163f7;hpb=b410cb21b726638c0618e1a0b420374a707fb64b;p=model-checker.git

diff --git a/model.h b/model.h
index 4fd2667..5a127b1 100644
--- a/model.h
+++ b/model.h
@@ -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;
 
@@ -255,6 +255,7 @@ private:
 	struct execution_stats stats;
 	void record_stats();
 
+	void print_infeasibility(const char *prefix) const;
 	bool is_feasible_prefix_ignore_relseq() const;
 	bool is_infeasible_ignoreRMW() const;
 	bool is_infeasible() const;