From: Brian Norris <banorris@uci.edu>
Date: Tue, 24 Apr 2012 03:18:44 +0000 (-0700)
Subject: tmp (model)
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=cc60d0e08cbe3bb8060bc535884574e347666a92;p=c11tester.git

tmp (model)
---

diff --git a/model.cc b/model.cc
index 4f87da3e..85ad11aa 100644
--- a/model.cc
+++ b/model.cc
@@ -30,6 +30,21 @@ ModelChecker::~ModelChecker()
 	delete rootNode;
 }
 
+void ModelChecker::reset_to_initial_state()
+{
+	DEBUG("+++ Resetting to initial state +++\n");
+	std::map<thread_id_t, class Thread *>::iterator it;
+	for (it = thread_map.begin(); it != thread_map.end(); it++) {
+		delete (*it).second;
+	}
+	thread_map.clear();
+	action_trace = new action_list_t();
+	currentNode = rootNode;
+	current_action = NULL;
+	used_thread_id = 1; // ?
+	/* scheduler reset ? */
+}
+
 int ModelChecker::get_next_id()
 {
 	return ++used_thread_id;
@@ -163,6 +178,16 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	backtrack_list.push_back(back);
 }
 
+Backtrack * ModelChecker::get_next_backtrack()
+{
+	Backtrack *next;
+	if (backtrack_list.empty())
+		return NULL;
+	next = backtrack_list.back();
+	backtrack_list.pop_back();
+	return next;
+}
+
 void ModelChecker::check_current_action(void)
 {
 	ModelAction *next = this->current_action;
diff --git a/model.h b/model.h
index ca1de85c..8cfd66f7 100644
--- a/model.h
+++ b/model.h
@@ -95,6 +95,8 @@ private:
 	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();
 
 	class ModelAction *current_action;
 	Backtrack *exploring;