6 /** @brief Node constructor */
7 Node::Node(ModelAction *act, Node *par, int nthreads)
10 num_threads(nthreads),
11 explored_children(num_threads),
12 backtrack(num_threads),
18 /** @brief Node desctructor */
25 /** Prints debugging info for the ModelAction associated with this Node */
31 printf("******** empty action ********\n");
35 * Checks if the Thread associated with this thread ID has been explored from
37 * @param tid is the thread ID to check
38 * @return true if this thread choice has been explored already, false
41 bool Node::has_been_explored(thread_id_t tid)
43 int id = id_to_int(tid);
44 return explored_children[id];
48 * Checks if the backtracking set is empty.
49 * @return true if the backtracking set is empty
51 bool Node::backtrack_empty()
53 return numBacktracks == 0;
57 * Explore a child Node using a given ModelAction. This updates both the
58 * Node-internal and the ModelAction data to associate the ModelAction with
60 * @param act is the ModelAction to explore
62 void Node::explore_child(ModelAction *act)
65 explore(act->get_tid());
69 * Records a backtracking reference for a thread choice within this Node.
70 * Provides feedback as to whether this thread choice is already set for
72 * @return false if the thread was already set to be backtracked, true
75 bool Node::set_backtrack(thread_id_t id)
77 int i = id_to_int(id);
85 thread_id_t Node::get_next_backtrack()
87 /* TODO: find next backtrack */
89 for (i = 0; i < backtrack.size(); i++)
90 if (backtrack[i] == true)
92 if (i >= backtrack.size())
93 return THREAD_ID_T_NONE;
99 bool Node::is_enabled(Thread *t)
101 return id_to_int(t->get_id()) < num_threads;
105 * Add an action to the may_read_from set.
106 * @param act is the action to add
108 void Node::add_read_from(ModelAction *act)
110 may_read_from.insert(act);
113 void Node::explore(thread_id_t tid)
115 int i = id_to_int(tid);
117 backtrack[i] = false;
120 explored_children[i] = true;
123 static void clear_node_list(node_list_t *list, node_list_t::iterator start,
124 node_list_t::iterator end)
126 node_list_t::iterator it;
128 for (it = start; it != end; it++)
130 list->erase(start, end);
133 NodeStack::NodeStack()
136 node_list.push_back(new Node());
138 iter = node_list.begin();
141 NodeStack::~NodeStack()
143 clear_node_list(&node_list, node_list.begin(), node_list.end());
146 void NodeStack::print()
148 node_list_t::iterator it;
149 printf("............................................\n");
150 printf("NodeStack printing node_list:\n");
151 for (it = node_list.begin(); it != node_list.end(); it++) {
152 if (it == this->iter)
153 printf("vvv following action is the current iterator vvv\n");
156 printf("............................................\n");
159 ModelAction * NodeStack::explore_action(ModelAction *act)
163 ASSERT(!node_list.empty());
165 if (get_head()->has_been_explored(act->get_tid())) {
167 return (*iter)->get_action();
170 /* Diverging from previous execution; clear out remainder of list */
171 node_list_t::iterator it = iter;
173 clear_node_list(&node_list, it, node_list.end());
176 get_head()->explore_child(act);
177 node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
183 Node * NodeStack::get_head()
185 if (node_list.empty())
190 Node * NodeStack::get_next()
192 node_list_t::iterator it = iter;
193 if (node_list.empty()) {
198 if (it == node_list.end()) {
205 void NodeStack::reset_execution()
207 iter = node_list.begin();