From 767599b6384b8b81044abd41c30cb1f5557fd068 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 14 May 2012 12:59:33 -0700 Subject: [PATCH] model: merge advance_backtracking_state() and get_next_replay_thread() --- model.cc | 27 +++++++++++---------------- model.h | 1 - 2 files changed, 11 insertions(+), 17 deletions(-) diff --git a/model.cc b/model.cc index a32fbe6..c19c37f 100644 --- 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 c8b3f76..8651a4f 100644 --- 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(); -- 2.34.1