From: Brian Norris <banorris@uci.edu>
Date: Tue, 16 Apr 2013 18:56:59 +0000 (-0700)
Subject: nodestack: register ModelExecution class w/in NodeStack
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f9e2e3a893918a431d3af1e6657cd08260e31941;p=cdsspec-compiler.git

nodestack: register ModelExecution class w/in NodeStack
---

diff --git a/execution.cc b/execution.cc
index 66418a4..33c862b 100644
--- a/execution.cc
+++ b/execution.cc
@@ -82,6 +82,7 @@ ModelExecution::ModelExecution(ModelChecker *m,
 	model_thread = new Thread(get_next_id());
 	add_thread(model_thread);
 	scheduler->register_engine(this);
+	node_stack->register_engine(this);
 }
 
 /** @brief Destructor */
diff --git a/nodestack.cc b/nodestack.cc
index f46e4b7..bfcf11f 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -9,6 +9,7 @@
 #include "model.h"
 #include "threads-model.h"
 #include "modeltypes.h"
+#include "execution.h"
 
 /**
  * @brief Node constructor
@@ -761,6 +762,15 @@ NodeStack::~NodeStack()
 		delete node_list[i];
 }
 
+/**
+ * @brief Register the model-checker object with this NodeStack
+ * @param exec The execution structure for the ModelChecker
+ */
+void NodeStack::register_engine(const ModelExecution *exec)
+{
+	this->execution = exec;
+}
+
 void NodeStack::print() const
 {
 	model_print("............................................\n");
diff --git a/nodestack.h b/nodestack.h
index e260f08..1a8bbbe 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -186,6 +186,9 @@ class NodeStack {
 public:
 	NodeStack();
 	~NodeStack();
+
+	void register_engine(const ModelExecution *exec);
+
 	ModelAction * explore_action(ModelAction *act, enabled_type_t * is_enabled);
 	Node * get_head() const;
 	Node * get_next() const;
@@ -199,6 +202,9 @@ public:
 private:
 	node_list_t node_list;
 
+	/** @brief The model-checker execution object */
+	const ModelExecution *execution;
+
 	/**
 	 * @brief the index position of the current head Node
 	 *