Make stack popping explicit.

[model-checker.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index 2416ed7c5b35d23deadd2f2681cd890a926e7f98..725bc5399f0fb84322b9ad90c161c8a386123fd4 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -109,8 +109,9 @@ thread_id_t Node::get_next_backtrack()
        for (i = 0; i < backtrack.size(); i++)
                if (backtrack[i] == true)
                        break;
-       if (i >= backtrack.size())
-               return THREAD_ID_T_NONE;
+       /* Backtrack set was empty? */
+       ASSERT(i != backtrack.size());
+
        backtrack[i] = false;
        numBacktracks--;
        return int_to_id(i);
@@ -197,17 +198,14 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        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();
        }
 
-       /* 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()));
@@ -216,6 +214,16 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        return NULL;
 }
 
+
+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())