snapshot-interface: cleanup interface header

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index f4da33071170beb37d21e55fbe21f498281a79a2..06fe72f87f7cd04c832a19dcc46c1f2bb0ebc7c1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -4,20 +4,13 @@
 #include "action.h"
 #include "nodestack.h"
 #include "schedule.h"
+#include "snapshot-interface.h"
 #include "common.h"
 
 #define INITIAL_THREAD_ID      0
 
 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 */
@@ -31,6 +24,7 @@ ModelChecker::ModelChecker()
        diverge(NULL),
        nextThread(THREAD_ID_T_NONE),
        action_trace(new action_list_t()),
+       thread_map(new std::map<int, class Thread *>),
        node_stack(new NodeStack()),
        next_backtrack(NULL)
 {
@@ -39,9 +33,9 @@ ModelChecker::ModelChecker()
 ModelChecker::~ModelChecker()
 {
        std::map<int, class Thread *>::iterator it;
-       for (it = thread_map.begin(); it != thread_map.end(); it++)
+       for (it = thread_map->begin(); it != thread_map->end(); it++)
                delete (*it).second;
-       thread_map.clear();
+       delete thread_map;
 
        delete action_trace;
 
@@ -52,19 +46,13 @@ ModelChecker::~ModelChecker()
 void ModelChecker::reset_to_initial_state()
 {
        DEBUG("+++ Resetting to initial state +++\n");
-       std::map<int, class Thread *>::iterator it;
-       for (it = thread_map.begin(); it != thread_map.end(); it++)
-               delete (*it).second;
-       thread_map.clear();
-       delete action_trace;
-       action_trace = new action_list_t();
        node_stack->reset_execution();
        current_action = NULL;
        next_thread_id = INITIAL_THREAD_ID;
        used_sequence_numbers = 0;
        nextThread = 0;
        next_backtrack = NULL;
-       /* scheduler reset ? */
+       snapshotObject->backTrackBeforeStep(0);
 }
 
 thread_id_t ModelChecker::get_next_id()
@@ -82,7 +70,7 @@ Thread * ModelChecker::schedule_next_thread()
        Thread *t;
        if (nextThread == THREAD_ID_T_NONE)
                return NULL;
-       t = thread_map[id_to_int(nextThread)];
+       t = (*thread_map)[id_to_int(nextThread)];
 
        ASSERT(t != NULL);
 
@@ -255,7 +243,7 @@ void ModelChecker::print_list(action_list_t *list)
 
 int ModelChecker::add_thread(Thread *t)
 {
-       thread_map[id_to_int(t->get_id())] = t;
+       (*thread_map)[id_to_int(t->get_id())] = t;
        scheduler->add_thread(t);
        return 0;
 }