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

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index aba3e8bc0c1783f87cad0c9b5b60b5ba9e3ae4c3..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();
 }
@@ -182,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)
@@ -189,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();
@@ -229,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);
 }