The current check will break in subtle ways as soon as we start to
add reads_from support as the thread selection is no longer the
only backtracking choice.
DEBUG("*** Divergence point ***\n");
tid = node->get_next_backtrack();
diverge = NULL;
DEBUG("*** Divergence point ***\n");
tid = node->get_next_backtrack();
diverge = NULL;
+ node_stack->pop_restofstack();
} else {
tid = next->get_tid();
}
} else {
tid = next->get_tid();
}
DBG();
ASSERT(!node_list.empty());
DBG();
ASSERT(!node_list.empty());
+ node_list_t::iterator it=iter;
+ it++;
- if (get_head()->has_been_explored(act->get_tid())) {
+ if (it != node_list.end()) {
iter++;
return (*iter)->get_action();
}
iter++;
return (*iter)->get_action();
}
- /* Diverging from previous execution; clear out remainder of list */
- node_list_t::iterator it = iter;
- it++;
- clear_node_list(&node_list, it, node_list.end());
-
/* Record action */
get_head()->explore_child(act);
node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
/* Record action */
get_head()->explore_child(act);
node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
+
+void NodeStack::pop_restofstack()
+{
+ /* Diverging from previous execution; clear out remainder of list */
+ node_list_t::iterator it = iter;
+ it++;
+ clear_node_list(&node_list, it, node_list.end());
+}
+
+
Node * NodeStack::get_head()
{
if (node_list.empty())
Node * NodeStack::get_head()
{
if (node_list.empty())
Node * get_head();
Node * get_next();
void reset_execution();
Node * get_head();
Node * get_next();
void reset_execution();
+ void pop_restofstack();
int get_total_nodes() { return total_nodes; }
void print();
int get_total_nodes() { return total_nodes; }
void print();