nodestack: register ModelExecution class w/in NodeStack
authorBrian Norris <banorris@uci.edu>
Tue, 16 Apr 2013 18:56:59 +0000 (11:56 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 16 Apr 2013 18:56:59 +0000 (11:56 -0700)
execution.cc
nodestack.cc
nodestack.h

index 66418a4..33c862b 100644 (file)
@@ -82,6 +82,7 @@ ModelExecution::ModelExecution(ModelChecker *m,
        model_thread = new Thread(get_next_id());
        add_thread(model_thread);
        scheduler->register_engine(this);
        model_thread = new Thread(get_next_id());
        add_thread(model_thread);
        scheduler->register_engine(this);
+       node_stack->register_engine(this);
 }
 
 /** @brief Destructor */
 }
 
 /** @brief Destructor */
index f46e4b7..bfcf11f 100644 (file)
@@ -9,6 +9,7 @@
 #include "model.h"
 #include "threads-model.h"
 #include "modeltypes.h"
 #include "model.h"
 #include "threads-model.h"
 #include "modeltypes.h"
+#include "execution.h"
 
 /**
  * @brief Node constructor
 
 /**
  * @brief Node constructor
@@ -761,6 +762,15 @@ NodeStack::~NodeStack()
                delete node_list[i];
 }
 
                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");
 void NodeStack::print() const
 {
        model_print("............................................\n");
index e260f08..1a8bbbe 100644 (file)
@@ -186,6 +186,9 @@ class NodeStack {
 public:
        NodeStack();
        ~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;
        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;
 
 private:
        node_list_t node_list;
 
+       /** @brief The model-checker execution object */
+       const ModelExecution *execution;
+
        /**
         * @brief the index position of the current head Node
         *
        /**
         * @brief the index position of the current head Node
         *