nodestack.cc

   1 #define __STDC_FORMAT_MACROS
   2 #include <inttypes.h>
   3 #include <cstdlib>
   4
   5 #include <string.h>
   6
   7 #include "nodestack.h"
   8 #include "action.h"
   9 #include "common.h"
  10 #include "threads-model.h"
  11 #include "modeltypes.h"
  12 #include "execution.h"
  13 #include "params.h"
  14
  15 /**
  16  * @brief Node constructor
  17  *
  18  * Constructs a single Node for use in a NodeStack. Each Node is associated
  19  * with exactly one ModelAction (exception: the first Node should be created
  20  * as an empty stub, to represent the first thread "choice") and up to one
  21  * parent.
  22  *
  23  * @param act The ModelAction to associate with this Node. May be NULL.
  24  * @param nthreads The number of threads which exist at this point in the
  25  * execution trace.
  26  */
  27 Node::Node(ModelAction *act) :
  28         action(act),
  29         uninit_action(NULL)
  30 {
  31         ASSERT(act);
  32         act->set_node(this);
  33 }
  34
  35 /** @brief Node desctructor */
  36 Node::~Node()
  37 {
  38         delete action;
  39         if (uninit_action)
  40                 delete uninit_action;
  41 }
  42
  43 /** Prints debugging info for the ModelAction associated with this Node */
  44 void Node::print() const
  45 {
  46         action->print();
  47 }
  48
  49 NodeStack::NodeStack() :
  50         node_list(),
  51         head_idx(-1)
  52 {
  53 }
  54
  55 NodeStack::~NodeStack()
  56 {
  57         for (unsigned int i = 0;i < node_list.size();i++)
  58                 delete node_list[i];
  59 }
  60
  61 /**
  62  * @brief Register the model-checker object with this NodeStack
  63  * @param exec The execution structure for the ModelChecker
  64  */
  65 void NodeStack::register_engine(const ModelExecution *exec)
  66 {
  67         this->execution = exec;
  68 }
  69
  70 const struct model_params * NodeStack::get_params() const
  71 {
  72         return execution->get_params();
  73 }
  74
  75 void NodeStack::print() const
  76 {
  77         model_print("............................................\n");
  78         model_print("NodeStack printing node_list:\n");
  79         for (unsigned int it = 0;it < node_list.size();it++) {
  80                 if ((int)it == this->head_idx)
  81                         model_print("vvv following action is the current iterator vvv\n");
  82                 node_list[it]->print();
  83         }
  84         model_print("............................................\n");
  85 }
  86
  87 /** Note: The is_enabled set contains what actions were enabled when
  88  *  act was chosen. */
  89 void NodeStack::add_action(ModelAction *act)
  90 {
  91         DBG();
  92
  93         node_list.push_back(new Node(act));
  94         head_idx++;
  95 }
  96
  97
  98 /** Reset the node stack. */
  99 void NodeStack::full_reset()
 100 {
 101         for (unsigned int i = 0;i < node_list.size();i++)
 102                 delete node_list[i];
 103         node_list.clear();
 104         reset_execution();
 105 }
 106
 107 Node * NodeStack::get_head() const
 108 {
 109         if (node_list.empty() || head_idx < 0)
 110                 return NULL;
 111         return node_list[head_idx];
 112 }
 113
 114 Node * NodeStack::get_next() const
 115 {
 116         if (node_list.empty()) {
 117                 DEBUG("Empty\n");
 118                 return NULL;
 119         }
 120         unsigned int it = head_idx + 1;
 121         if (it == node_list.size()) {
 122                 DEBUG("At end\n");
 123                 return NULL;
 124         }
 125         return node_list[it];
 126 }
 127
 128 void NodeStack::reset_execution()
 129 {
 130         head_idx = -1;
 131 }