6 int Node::total_nodes = 0;
8 Node::Node(ModelAction *act, int nthreads)
10 num_threads(nthreads),
11 explored_children(num_threads),
12 backtrack(num_threads)
28 printf("******** empty action ********\n");
31 bool Node::has_been_explored(thread_id_t tid)
33 int id = id_to_int(tid);
34 return explored_children[id];
37 bool Node::backtrack_empty()
40 for (i = 0; i < backtrack.size(); i++)
41 if (backtrack[i] == true)
46 void Node::explore_child(ModelAction *act)
49 explore(act->get_tid());
52 bool Node::set_backtrack(thread_id_t id)
54 int i = id_to_int(id);
61 thread_id_t Node::get_next_backtrack()
63 /* TODO: find next backtrack */
65 for (i = 0; i < backtrack.size(); i++)
66 if (backtrack[i] == true)
68 if (i >= backtrack.size())
69 return THREAD_ID_T_NONE;
74 bool Node::is_enabled(Thread *t)
76 return id_to_int(t->get_id()) < num_threads;
79 void Node::explore(thread_id_t tid)
81 int i = id_to_int(tid);
83 explored_children[i] = true;
86 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
87 node_list_t::iterator end)
89 node_list_t::iterator it;
91 for (it = start; it != end; it++)
93 list->erase(start, end);
96 NodeStack::NodeStack()
98 node_list.push_back(new Node());
99 iter = node_list.begin();
102 NodeStack::~NodeStack()
104 clear_node_list(&node_list, node_list.begin(), node_list.end());
107 void NodeStack::print()
109 node_list_t::iterator it;
110 printf("............................................\n");
111 printf("NodeStack printing node_list:\n");
112 for (it = node_list.begin(); it != node_list.end(); it++) {
113 if (it == this->iter)
114 printf("vvv following action is the current iterator vvv\n");
117 printf("............................................\n");
120 ModelAction * NodeStack::explore_action(ModelAction *act, ModelAction *parent)
124 ASSERT(!node_list.empty());
126 if (get_head()->has_been_explored(act->get_tid())) {
127 /* Discard duplicate ModelAction */
130 } else { /* Diverging from previous execution */
131 /* Clear out remainder of list */
132 node_list_t::iterator it = iter;
134 clear_node_list(&node_list, it, node_list.end());
137 get_head()->explore_child(act);
138 act->create_cv(parent);
139 node_list.push_back(new Node(act, model->get_num_threads()));
142 return (*iter)->get_action();
145 Node * NodeStack::get_head()
147 if (node_list.empty())
152 Node * NodeStack::get_next()
154 node_list_t::iterator it = iter;
155 if (node_list.empty()) {
160 if (it == node_list.end()) {
167 void NodeStack::reset_execution()
169 iter = node_list.begin();