From: Brian Norris <banorris@uci.edu>
Date: Thu, 3 May 2012 18:46:27 +0000 (-0700)
Subject: model: move class Backtrack to model.cc
X-Git-Tag: pldi2013~463
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=a6017fe478a3087152beb4b7d3da99b3be54d41c;p=model-checker.git

model: move class Backtrack to model.cc

Backtrack is only used within model.{cc,h}, so make it an "inner class."
---

diff --git a/model.cc b/model.cc
index e0c16eb..7a29e00 100644
--- a/model.cc
+++ b/model.cc
@@ -8,6 +8,26 @@
 
 #define INITIAL_THREAD_ID	0
 
+class Backtrack {
+public:
+	Backtrack(ModelAction *d, action_list_t *t) {
+		diverge = d;
+		actionTrace = t;
+		iter = actionTrace->begin();
+	}
+	ModelAction * get_diverge() { return diverge; }
+	action_list_t * get_trace() { return actionTrace; }
+	void advance_state() { iter++; }
+	ModelAction * get_state() {
+		return iter == actionTrace->end() ? NULL : *iter;
+	}
+private:
+	ModelAction *diverge;
+	action_list_t *actionTrace;
+	/* points to position in actionTrace as we replay */
+	action_list_t::iterator iter;
+};
+
 ModelChecker *model;
 
 ModelChecker::ModelChecker()
diff --git a/model.h b/model.h
index 2933f54..c8b3f76 100644
--- a/model.h
+++ b/model.h
@@ -14,26 +14,7 @@
 
 /* Forward declaration */
 class TreeNode;
-
-class Backtrack {
-public:
-	Backtrack(ModelAction *d, action_list_t *t) {
-		diverge = d;
-		actionTrace = t;
-		iter = actionTrace->begin();
-	}
-	ModelAction * get_diverge() { return diverge; }
-	action_list_t * get_trace() { return actionTrace; }
-	void advance_state() { iter++; }
-	ModelAction * get_state() {
-		return iter == actionTrace->end() ? NULL : *iter;
-	}
-private:
-	ModelAction *diverge;
-	action_list_t *actionTrace;
-	/* points to position in actionTrace as we replay */
-	action_list_t::iterator iter;
-};
+class Backtrack;
 
 class ModelChecker {
 public: