add documentation

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 93e06d0262de2b4c4d93bf8c9207f018b710cb3e..f12e4d27db44af7b3593067c806c539ce930ced9 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -124,7 +124,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
        next = node_stack->get_next()->get_action();
 
        if (next == diverge) {
-               Node *node = next->get_node();
+               Node *node = next->get_node()->get_parent();
 
                /* Reached divergence point */
                DEBUG("*** Divergence point ***\n");
@@ -196,7 +196,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
        if (prev == NULL)
                return;
 
-       node = prev->get_node();
+       node = prev->get_node()->get_parent();
 
        while (!node->is_enabled(t))
                t = t->get_parent();
@@ -205,6 +205,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
        if (node->has_been_explored(t->get_id()))
                return;
 
+       /* Cache the latest backtracking point */
        if (!next_backtrack || *prev > *next_backtrack)
                next_backtrack = prev;
 
@@ -262,7 +263,7 @@ void ModelChecker::check_current_action(void)
 
        nextThread = get_next_replay_thread();
 
-       currnode = curr->get_node();
+       currnode = curr->get_node()->get_parent();
 
        if (!currnode->backtrack_empty())
                if (!next_backtrack || *curr > *next_backtrack)