nodestack: compute parent ModelAction externally

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index f4da33071170beb37d21e55fbe21f498281a79a2..42f412f421e389267d58d1ce6fba9c6d9fb44cf2 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,8 @@ ModelChecker::ModelChecker()
        diverge(NULL),
        nextThread(THREAD_ID_T_NONE),
        action_trace(new action_list_t()),
+       thread_map(new std::map<int, class Thread *>),
+       obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
        node_stack(new NodeStack()),
        next_backtrack(NULL)
 {
@@ -39,12 +34,12 @@ 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 obj_thrd_map;
        delete action_trace;
-
        delete node_stack;
        delete scheduler;
 }
@@ -52,19 +47,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()
@@ -72,6 +61,11 @@ thread_id_t ModelChecker::get_next_id()
        return next_thread_id++;
 }
 
+int ModelChecker::get_num_threads()
+{
+       return next_thread_id;
+}
+
 int ModelChecker::get_next_seq_num()
 {
        return ++used_sequence_numbers;
@@ -82,7 +76,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);
 
@@ -215,7 +209,7 @@ void ModelChecker::check_current_action(void)
                return;
        }
 
-       curr = node_stack->explore_action(curr);
+       curr = node_stack->explore_action(curr, NULL);
        nextThread = get_next_replay_thread();
 
        currnode = curr->get_node();
@@ -226,6 +220,11 @@ void ModelChecker::check_current_action(void)
 
        set_backtracking(curr);
        this->action_trace->push_back(curr);
+
+       std::vector<action_list_t> *vec = &(*obj_thrd_map)[curr->get_location()];
+       if (id_to_int(curr->get_tid()) >= (int)vec->size())
+               vec->resize(next_thread_id);
+       (*vec)[id_to_int(curr->get_tid())].push_back(curr);
 }
 
 void ModelChecker::print_summary(void)
@@ -255,7 +254,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;
 }