bugfix - set backtrack events according to an *enabled* thread

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 7a29e00b6e2be472dd519e7674fa43769f998499..e3238258a3aa86b0570ff8ed8159eb62e27a899c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -43,7 +43,7 @@ ModelChecker::ModelChecker()
        this->exploring = NULL;
        this->nextThread = THREAD_ID_T_NONE;
 
-       rootNode = new TreeNode(NULL);
+       rootNode = new TreeNode();
        currentNode = rootNode;
        action_trace = new action_list_t();
 }
@@ -142,14 +142,15 @@ bool ModelChecker::next_execution()
        print_summary();
        if ((exploring = model->get_next_backtrack()) == NULL)
                return false;
-       model->reset_to_initial_state();
-       nextThread = get_next_replay_thread();
 
        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
                exploring->get_diverge()->print();
                print_list(exploring->get_trace());
        }
+
+       model->reset_to_initial_state();
+       nextThread = get_next_replay_thread();
        return true;
 }
 
@@ -181,6 +182,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 {
        ModelAction *prev;
        TreeNode *node;
+       Thread *t = get_thread(act->get_tid());
 
        prev = get_last_conflict(act);
        if (prev == NULL)
@@ -188,15 +190,18 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
        node = prev->get_node();
 
+       while (t && !node->is_enabled(t))
+               t = t->get_parent();
+
        /* Check if this has been explored already */
-       if (node->hasBeenExplored(act->get_tid()))
+       if (node->hasBeenExplored(t->get_id()))
                return;
        /* If this is a new backtracking point, mark the tree */
-       if (node->setBacktrack(act->get_tid()) != 0)
+       if (node->setBacktrack(t->get_id()) != 0)
                return;
 
        DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-                       prev->get_tid(), act->get_tid());
+                       prev->get_tid(), t->get_id());
        if (DBG_ENABLED()) {
                prev->print();
                act->print();
@@ -228,7 +233,7 @@ void ModelChecker::check_current_action(void)
        nextThread = advance_backtracking_state();
        next->set_node(currentNode);
        set_backtracking(next);
-       currentNode = currentNode->exploreChild(next->get_tid());
+       currentNode = currentNode->explore_child(next);
        this->action_trace->push_back(next);
 }