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)
{
delete (*it).second;
delete thread_map;
+ delete obj_thrd_map;
delete action_trace;
-
delete node_stack;
delete scheduler;
}
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);
}
return next_thread_id++;
}
+int ModelChecker::get_num_threads()
+{
+ return next_thread_id;
+}
+
int ModelChecker::get_next_seq_num()
{
return ++used_sequence_numbers;
return;
}
- curr = node_stack->explore_action(curr);
+ curr = node_stack->explore_action(curr, NULL);
nextThread = get_next_replay_thread();
currnode = curr->get_node();
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)