X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.h;h=c3e5830211c9276ec7b5004504fbb9472df32069;hp=1b6bb10a285e4046e4b9bbe727526abf1849f071;hb=50b95c3747f4fe79b2ab1a1a6fc303224e16e418;hpb=f2a014110185c734180545ffc1dc2f0dcd30fd0c;ds=sidebyside

diff --git a/model.h b/model.h
index 1b6bb10..c3e5830 100644
--- a/model.h
+++ b/model.h
@@ -28,6 +28,7 @@ class Promise;
  * the model checker.
  */
 struct model_params {
+	int maxreads;
 };
 
 /**
@@ -100,9 +101,11 @@ private:
 	 */
 	void set_current_action(ModelAction *act) { priv->current_action = act; }
 	Thread * check_current_action(ModelAction *curr);
+	bool process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw);
 
 	bool take_step();
 
+	void check_recency(ModelAction *curr, bool already_added);
 	ModelAction * get_last_conflict(ModelAction *act);
 	void set_backtracking(ModelAction *act);
 	Thread * get_next_thread(ModelAction *curr);
@@ -176,6 +179,7 @@ private:
 	 */
 	CycleGraph *mo_graph;
 	bool failed_promise;
+	bool too_many_reads;
 	bool asserted;
 };