Merge commit: branch 'work'

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index e5af1a6f328e729ffe7885071a42c1a70dc4581a..8da05aae2be481e348b4b5b9f3de6e08384ff523 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -4,40 +4,14 @@
 #include "action.h"
 #include "nodestack.h"
 #include "schedule.h"
+#include "snapshot-interface.h"
+#undef DEBUG
 #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 */
@@ -58,7 +32,7 @@ ModelChecker::ModelChecker()
 
 ModelChecker::~ModelChecker()
 {
-       std::map<int, class Thread *>::iterator it;
+       std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
        for (it = thread_map.begin(); it != thread_map.end(); it++)
                delete (*it).second;
        thread_map.clear();
@@ -72,7 +46,7 @@ ModelChecker::~ModelChecker()
 void ModelChecker::reset_to_initial_state()
 {
        DEBUG("+++ Resetting to initial state +++\n");
-       std::map<int, class Thread *>::iterator it;
+       std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
        for (it = thread_map.begin(); it != thread_map.end(); it++)
                delete (*it).second;
        thread_map.clear();