nodestack: register ModelExecution class w/in NodeStack

diff --git a/execution.cc b/execution.cc
index 66418a4abb630a5b234b035342f4179435c52363..33c862bac36fd2a7e788cfae00a1a46a774ecd4a 100644 (file)
--- 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 f46e4b75571fd03b414760413bc68beff897f16f..bfcf11ff6dafb0f525b92b202e5401b5f3ce046f 100644 (file)
--- 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 e260f083c80a9455cabf4f0c23c3d30e0c9ccb1c..1a8bbbe9f371cc2bef422ec2218e96f989fb28a8 100644 (file)
--- 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
         *