clockvector: add ClockVector class

[model-checker.git] / model.h

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: