X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.h;h=e6dc06ddd97c2aef7d7c7dd17ae71854162ffb5e;hp=41ec97b50bdb71744075d0216a4bb209813255a9;hb=5e4a7d161cba81152ddcf295ee72fbb25ba3afaa;hpb=bdef0741b8a01e16946d261bc2a657af5a683b3e

diff --git a/model.h b/model.h
index 41ec97b5..e6dc06dd 100644
--- a/model.h
+++ b/model.h
@@ -57,6 +57,7 @@ public:
 	ClockVector * get_cv(thread_id_t tid);
 	bool next_execution();
 	bool isfeasible();
+	void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
 
 	MEMALLOC
 private:
@@ -86,8 +87,7 @@ private:
 	ModelAction * process_rmw(ModelAction * curr);
 	void r_modification_order(ModelAction * curr, const ModelAction *rf);
 	void w_modification_order(ModelAction * curr);
-
-
+	
 	ModelAction *current_action;
 	ModelAction *diverge;
 	thread_id_t nextThread;
@@ -106,6 +106,7 @@ private:
 	NodeStack *node_stack;
 	ModelAction *next_backtrack;
 	CycleGraph * cyclegraph;
+	bool failed_promise;
 };
 
 extern ModelChecker *model;