X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=62be08746db8ad95fe4aa09283c2f2034250a750;hb=a2b1ce7713d29dd465afc54660781aa04dc7db59;hp=e5af1a6f328e729ffe7885071a42c1a70dc4581a;hpb=a23393a8fa54e0318f3958838acbdec6d5d3d82a;p=model-checker.git

diff --git a/model.cc b/model.cc
index e5af1a6..62be087 100644
--- a/model.cc
+++ b/model.cc
@@ -4,40 +4,13 @@
 #include "action.h"
 #include "nodestack.h"
 #include "schedule.h"
+#include "snapshot-interface.h"
 #include "common.h"
 
 #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;
 
-void free_action_list(action_list_t *list)
-{
-	action_list_t::iterator it;
-	for (it = list->begin(); it != list->end(); it++)
-		delete (*it);
-	delete list;
-}
-
 ModelChecker::ModelChecker()
 	:
 	/* Initialize default scheduler */