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

diff --git a/model.h b/model.h
index a8268cf..7bc3585 100644
--- a/model.h
+++ b/model.h
@@ -124,7 +124,8 @@ private:
 	int num_executions;
 	int num_feasible_executions;
 	bool promises_expired();
-
+	void execute_sleep_set();
+	void wake_up_sleeping_actions(ModelAction * curr);
 	modelclock_t get_next_seq_num();
 
 	/**
@@ -140,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();
@@ -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
 	 *