1 #define __STDC_FORMAT_MACROS
10 #include "threads-model.h"
11 #include "modeltypes.h"
12 #include "execution.h"
16 * @brief Node constructor
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
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
27 Node::Node(ModelAction *act) :
35 /** @brief Node desctructor */
43 /** Prints debugging info for the ModelAction associated with this Node */
44 void Node::print() const
49 NodeStack::NodeStack() :
55 NodeStack::~NodeStack()
57 for (unsigned int i = 0;i < node_list.size();i++)
62 * @brief Register the model-checker object with this NodeStack
63 * @param exec The execution structure for the ModelChecker
65 void NodeStack::register_engine(const ModelExecution *exec)
67 this->execution = exec;
70 const struct model_params * NodeStack::get_params() const
72 return execution->get_params();
75 void NodeStack::print() const
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();
84 model_print("............................................\n");
87 /** Note: The is_enabled set contains what actions were enabled when
89 ModelAction * NodeStack::explore_action(ModelAction *act)
93 node_list.push_back(new Node(act));
99 /** Reset the node stack. */
100 void NodeStack::full_reset()
102 for (unsigned int i = 0;i < node_list.size();i++)
108 Node * NodeStack::get_head() const
110 if (node_list.empty() || head_idx < 0)
112 return node_list[head_idx];
115 Node * NodeStack::get_next() const
117 if (node_list.empty()) {
121 unsigned int it = head_idx + 1;
122 if (it == node_list.size()) {
126 return node_list[it];
129 void NodeStack::reset_execution()