nodestack: compute parent ModelAction externally

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 62be08746db8ad95fe4aa09283c2f2034250a750..42f412f421e389267d58d1ce6fba9c6d9fb44cf2 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -24,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)
 {
@@ -32,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;
 }
@@ -45,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()
@@ -65,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;
@@ -75,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);
 
@@ -208,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();
@@ -219,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)
@@ -248,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;
 }