X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.h;h=7bc3585d8562eeff369cf307b81751781e381f6b;hp=d2baaf45afee14661a02c620649e4efdfcf107ee;hb=b8b39c87557325a384faa45d0cae56a6f71f52b1;hpb=59eb730e1d19a0825008c40eb521bfc5c29df5f9

diff --git a/model.h b/model.h
index d2baaf4..7bc3585 100644
--- a/model.h
+++ b/model.h
@@ -141,6 +141,7 @@ private:
 	bool process_write(ModelAction *curr);
 	bool process_mutex(ModelAction *curr);
 	bool process_thread_action(ModelAction *curr);
+	void process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue);
 	bool check_action_enabled(ModelAction *curr);
 
 	bool take_step();
@@ -153,6 +154,7 @@ private:
 	void reset_to_initial_state();
 	bool resolve_promises(ModelAction *curr);
 	void compute_promises(ModelAction *curr);
+	void compute_relseq_breakwrites(ModelAction *curr);
 
 	void check_curr_backtracking(ModelAction * curr);
 	void add_action_to_lists(ModelAction *act);
@@ -202,6 +204,10 @@ private:
 	 * together for efficiency and maintainability. */
 	struct model_snapshot_members *priv;
 
+	/** A special model-checker Thread; used for associating with
+	 *  model-checker-related ModelAcitons */
+	Thread *model_thread;
+
 	/**
 	 * @brief The modification order graph
 	 *