5 int Node::total_nodes = 0;
7 Node::Node(ModelAction *act, Node *parent)
9 num_threads(parent ? parent->num_threads : 1),
10 explored_children(num_threads),
11 backtrack(num_threads)
14 if (act && act->get_type() == THREAD_CREATE) {
16 explored_children.resize(num_threads);
17 backtrack.resize(num_threads);
32 printf("******** empty action ********\n");
35 bool Node::has_been_explored(thread_id_t tid)
37 int id = id_to_int(tid);
38 return explored_children[id];
41 bool Node::backtrack_empty()
44 for (i = 0; i < backtrack.size(); i++)
45 if (backtrack[i] == true)
50 void Node::explore_child(ModelAction *act)
53 explore(act->get_tid());
56 bool Node::set_backtrack(thread_id_t id)
58 int i = id_to_int(id);
65 thread_id_t Node::get_next_backtrack()
67 /* TODO: find next backtrack */
69 for (i = 0; i < backtrack.size(); i++)
70 if (backtrack[i] == true)
72 if (i >= backtrack.size())
73 return THREAD_ID_T_NONE;
78 bool Node::is_enabled(Thread *t)
80 return id_to_int(t->get_id()) < num_threads;
83 void Node::explore(thread_id_t tid)
85 int i = id_to_int(tid);
87 explored_children[i] = true;
90 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
91 node_list_t::iterator end)
93 node_list_t::iterator it;
95 for (it = start; it != end; it++)
97 list->erase(start, end);
100 NodeStack::NodeStack()
102 node_list.push_back(new Node());
103 iter = node_list.begin();
106 NodeStack::~NodeStack()
108 clear_node_list(&node_list, node_list.begin(), node_list.end());
111 void NodeStack::print()
113 node_list_t::iterator it;
114 printf("............................................\n");
115 printf("NodeStack printing node_list:\n");
116 for (it = node_list.begin(); it != node_list.end(); it++) {
117 if (it == this->iter)
118 printf("vvv following action is the current iterator vvv\n");
121 printf("............................................\n");
124 ModelAction * NodeStack::explore_action(ModelAction *act)
128 ASSERT(!node_list.empty());
130 if (get_head()->has_been_explored(act->get_tid())) {
131 /* Discard duplicate ModelAction */
134 } else { /* Diverging from previous execution */
135 /* Clear out remainder of list */
136 node_list_t::iterator it = iter;
138 clear_node_list(&node_list, it, node_list.end());
141 get_head()->explore_child(act);
142 node_list.push_back(new Node(act, get_head()));
145 return (*iter)->get_action();
148 Node * NodeStack::get_head()
150 if (node_list.empty())
155 Node * NodeStack::get_next()
157 node_list_t::iterator it = iter;
158 if (node_list.empty()) {
163 if (it == node_list.end()) {
170 void NodeStack::reset_execution()
172 iter = node_list.begin();