model: merge advance_backtracking_state() and get_next_replay_thread()

diff --git a/model.cc b/model.cc
index a32fbe61b3bc54405f3ee9f10881520b98e8be7f..c19c37f0cdc778684d6796842043a7b71afee440 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -81,6 +81,7 @@ void ModelChecker::reset_to_initial_state()
        current_action = NULL;
        next_thread_id = INITIAL_THREAD_ID;
        used_sequence_numbers = 0;
+       nextThread = 0;
        /* scheduler reset ? */
 }
 
@@ -118,6 +119,15 @@ thread_id_t ModelChecker::get_next_replay_thread()
        ModelAction *next;
        thread_id_t tid;
 
+       /* Have we completed exploring the preselected path? */
+       if (exploring == NULL)
+               return THREAD_ID_T_NONE;
+
+       /* Else, we are trying to replay an execution */
+       exploring->advance_state();
+
+       ASSERT(exploring->get_state() != NULL);
+
        next = exploring->get_state();
 
        if (next == exploring->get_diverge()) {
@@ -135,20 +145,6 @@ thread_id_t ModelChecker::get_next_replay_thread()
        return tid;
 }
 
-thread_id_t ModelChecker::advance_backtracking_state()
-{
-       /* Have we completed exploring the preselected path? */
-       if (exploring == NULL)
-               return THREAD_ID_T_NONE;
-
-       /* Else, we are trying to replay an execution */
-       exploring->advance_state();
-
-       ASSERT(exploring->get_state() != NULL);
-
-       return get_next_replay_thread();
-}
-
 bool ModelChecker::next_execution()
 {
        DBG();
@@ -165,7 +161,6 @@ bool ModelChecker::next_execution()
        }
 
        model->reset_to_initial_state();
-       nextThread = get_next_replay_thread();
        return true;
 }
 
@@ -245,7 +240,7 @@ void ModelChecker::check_current_action(void)
                return;
        }
 
-       nextThread = advance_backtracking_state();
+       nextThread = get_next_replay_thread();
        curr->set_node(currentNode);
        set_backtracking(curr);
        currentNode = currentNode->explore_child(curr);

diff --git a/model.h b/model.h
index c8b3f762035751ed66c6d4bd772c9066a3bc2183..8651a4f9ffe166125571920414dff6999a009798 100644 (file)
--- a/model.h
+++ b/model.h
@@ -47,7 +47,6 @@ private:
 
        ModelAction * get_last_conflict(ModelAction *act);
        void set_backtracking(ModelAction *act);
-       thread_id_t advance_backtracking_state();
        thread_id_t get_next_replay_thread();
        Backtrack * get_next_backtrack();
        void reset_to_initial_state();