6 /** @brief Node constructor */
7 Node::Node(ModelAction *act, int nthreads)
10 explored_children(num_threads),
11 backtrack(num_threads),
17 /** @brief Node desctructor */
24 /** Prints debugging info for the ModelAction associated with this Node */
30 printf("******** empty action ********\n");
34 * Checks if the Thread associated with this thread ID has been explored from
36 * @param tid is the thread ID to check
37 * @return true if this thread choice has been explored already, false
40 bool Node::has_been_explored(thread_id_t tid)
42 int id = id_to_int(tid);
43 return explored_children[id];
47 * Checks if the backtracking set is empty.
48 * @return true if the backtracking set is empty
50 bool Node::backtrack_empty()
52 return numBacktracks == 0;
56 * Explore a child Node using a given ModelAction. This updates both the
57 * Node-internal and the ModelAction data to associate the ModelAction with
59 * @param act is the ModelAction to explore
61 void Node::explore_child(ModelAction *act)
64 explore(act->get_tid());
68 * Records a backtracking reference for a thread choice within this Node.
69 * Provides feedback as to whether this thread choice is already set for
71 * @return false if the thread was already set to be backtracked, true
74 bool Node::set_backtrack(thread_id_t id)
76 int i = id_to_int(id);
84 thread_id_t Node::get_next_backtrack()
86 /* TODO: find next backtrack */
88 for (i = 0; i < backtrack.size(); i++)
89 if (backtrack[i] == true)
91 if (i >= backtrack.size())
92 return THREAD_ID_T_NONE;
98 bool Node::is_enabled(Thread *t)
100 return id_to_int(t->get_id()) < num_threads;
104 * Add an action to the may_read_from set.
105 * @param act is the action to add
107 void Node::add_read_from(ModelAction *act)
109 may_read_from.insert(act);
112 void Node::explore(thread_id_t tid)
114 int i = id_to_int(tid);
116 backtrack[i] = false;
119 explored_children[i] = true;
122 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
123 node_list_t::iterator end)
125 node_list_t::iterator it;
127 for (it = start; it != end; it++)
129 list->erase(start, end);
132 NodeStack::NodeStack()
135 node_list.push_back(new Node());
137 iter = node_list.begin();
140 NodeStack::~NodeStack()
142 clear_node_list(&node_list, node_list.begin(), node_list.end());
145 void NodeStack::print()
147 node_list_t::iterator it;
148 printf("............................................\n");
149 printf("NodeStack printing node_list:\n");
150 for (it = node_list.begin(); it != node_list.end(); it++) {
151 if (it == this->iter)
152 printf("vvv following action is the current iterator vvv\n");
155 printf("............................................\n");
158 ModelAction * NodeStack::explore_action(ModelAction *act)
162 ASSERT(!node_list.empty());
164 if (get_head()->has_been_explored(act->get_tid())) {
166 return (*iter)->get_action();
169 /* Diverging from previous execution; clear out remainder of list */
170 node_list_t::iterator it = iter;
172 clear_node_list(&node_list, it, node_list.end());
175 get_head()->explore_child(act);
176 node_list.push_back(new Node(act, model->get_num_threads()));
182 Node * NodeStack::get_head()
184 if (node_list.empty())
189 Node * NodeStack::get_next()
191 node_list_t::iterator it = iter;
192 if (node_list.empty()) {
197 if (it == node_list.end()) {
204 void NodeStack::reset_execution()
206 iter = node_list.begin();