X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.h;h=616a47cb47a4e34c182359e0217724b2808e59ad;hb=7bfea91f33595532cf618fe3d090e8021f578795;hp=0f1e8aed1e243dc3a05d4b7fa666e33fca400c71;hpb=f9fe0087091f88deeb814d0768eecdfb1b51a94d;p=model-checker.git

diff --git a/execution.h b/execution.h
index 0f1e8ae..616a47c 100644
--- a/execution.h
+++ b/execution.h
@@ -60,7 +60,10 @@ struct release_seq {
 /** @brief The central structure for model-checking */
 class ModelExecution {
 public:
-	ModelExecution(struct model_params *params, Scheduler *scheduler, NodeStack *node_stack);
+	ModelExecution(ModelChecker *m,
+			struct model_params *params,
+			Scheduler *scheduler,
+			NodeStack *node_stack);
 	~ModelExecution();
 
 	Thread * take_step(ModelAction *curr);
@@ -110,10 +113,12 @@ public:
 
 	action_list_t * get_action_trace() const { return action_trace; }
 
-	void increment_execution_number() { execution_number++; }
-
 	MEMALLOC
 private:
+	int get_execution_number() const;
+
+	ModelChecker *model;
+
 	const model_params * const params;
 
 	/** The scheduler to use: tracks the running/ready Threads */
@@ -231,8 +236,6 @@ private:
 	 */
 	CycleGraph * const mo_graph;
 
-	int execution_number;
-
 	Thread * action_select_next_thread(const ModelAction *curr) const;
 };