6 Node::Node(ModelAction *act, int nthreads)
9 explored_children(num_threads),
10 backtrack(num_threads)
25 printf("******** empty action ********\n");
28 bool Node::has_been_explored(thread_id_t tid)
30 int id = id_to_int(tid);
31 return explored_children[id];
34 bool Node::backtrack_empty()
37 for (i = 0; i < backtrack.size(); i++)
38 if (backtrack[i] == true)
43 void Node::explore_child(ModelAction *act)
46 explore(act->get_tid());
49 bool Node::set_backtrack(thread_id_t id)
51 int i = id_to_int(id);
58 thread_id_t Node::get_next_backtrack()
60 /* TODO: find next backtrack */
62 for (i = 0; i < backtrack.size(); i++)
63 if (backtrack[i] == true)
65 if (i >= backtrack.size())
66 return THREAD_ID_T_NONE;
71 bool Node::is_enabled(Thread *t)
73 return id_to_int(t->get_id()) < num_threads;
76 void Node::explore(thread_id_t tid)
78 int i = id_to_int(tid);
80 explored_children[i] = true;
83 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
84 node_list_t::iterator end)
86 node_list_t::iterator it;
88 for (it = start; it != end; it++)
90 list->erase(start, end);
93 NodeStack::NodeStack()
96 node_list.push_back(new Node());
98 iter = node_list.begin();
101 NodeStack::~NodeStack()
103 clear_node_list(&node_list, node_list.begin(), node_list.end());
106 void NodeStack::print()
108 node_list_t::iterator it;
109 printf("............................................\n");
110 printf("NodeStack printing node_list:\n");
111 for (it = node_list.begin(); it != node_list.end(); it++) {
112 if (it == this->iter)
113 printf("vvv following action is the current iterator vvv\n");
116 printf("............................................\n");
119 ModelAction * NodeStack::explore_action(ModelAction *act)
123 ASSERT(!node_list.empty());
125 if (get_head()->has_been_explored(act->get_tid())) {
126 /* Discard duplicate ModelAction */
129 } else { /* Diverging from previous execution */
130 /* Clear out remainder of list */
131 node_list_t::iterator it = iter;
133 clear_node_list(&node_list, it, node_list.end());
136 get_head()->explore_child(act);
137 node_list.push_back(new Node(act, model->get_num_threads()));
141 return (*iter)->get_action();
144 Node * NodeStack::get_head()
146 if (node_list.empty())
151 Node * NodeStack::get_next()
153 node_list_t::iterator it = iter;
154 if (node_list.empty()) {
159 if (it == node_list.end()) {
166 void NodeStack::reset_execution()
168 iter = node_list.begin();