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 e0c16eba8e1ac0677c3a6de32d6e94230d949c37..7a29e00b6e2be472dd519e7674fa43769f998499 100644 (file)
--- 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 2933f54cd7e5d4571c94f36ed4f652a3d34dcd1c..c8b3f762035751ed66c6d4bd772c9066a3bc2183 100644 (file)
--- 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: