From: Brian Norris <banorris@uci.edu>
Date: Mon, 14 May 2012 19:59:33 +0000 (-0700)
Subject: model: merge advance_backtracking_state() and get_next_replay_thread()
X-Git-Tag: pldi2013~441
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=767599b6384b8b81044abd41c30cb1f5557fd068;p=model-checker.git

model: merge advance_backtracking_state() and get_next_replay_thread()
---

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();