From a6017fe478a3087152beb4b7d3da99b3be54d41c Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 3 May 2012 11:46:27 -0700 Subject: [PATCH] model: move class Backtrack to model.cc Backtrack is only used within model.{cc,h}, so make it an "inner class." --- model.cc | 20 ++++++++++++++++++++ model.h | 21 +-------------------- 2 files changed, 21 insertions(+), 20 deletions(-) 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: -- 2.34.1