#include "action.h"
#include "tree.h"
#include "schedule.h"
+#include "snapshot-interface.h"
+#undef DEBUG
#include "common.h"
#define INITIAL_THREAD_ID 0
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();
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();
current_action = NULL;
next_thread_id = INITIAL_THREAD_ID;
used_sequence_numbers = 0;
+ nextThread = 0;
/* scheduler reset ? */
}
ModelAction *next;
thread_id_t tid;
+ /* Have we completed exploring the preselected path? */
+ if (exploring == NULL)
+ return THREAD_ID_T_NONE;
+
+ /* Else, we are trying to replay an execution */
+ exploring->advance_state();
+
+ ASSERT(exploring->get_state() != NULL);
+
next = exploring->get_state();
if (next == exploring->get_diverge()) {
return tid;
}
-thread_id_t ModelChecker::advance_backtracking_state()
-{
- /* Have we completed exploring the preselected path? */
- if (exploring == NULL)
- return THREAD_ID_T_NONE;
-
- /* Else, we are trying to replay an execution */
- exploring->advance_state();
-
- ASSERT(exploring->get_state() != NULL);
-
- return get_next_replay_thread();
-}
-
bool ModelChecker::next_execution()
{
DBG();
}
model->reset_to_initial_state();
- nextThread = get_next_replay_thread();
return true;
}
void ModelChecker::check_current_action(void)
{
- ModelAction *next = this->current_action;
-
- if (!next) {
+ ModelAction *curr = this->current_action;
+ current_action = NULL;
+ if (!curr) {
DEBUG("trying to push NULL action...\n");
return;
}
- current_action = NULL;
- nextThread = advance_backtracking_state();
- next->set_node(currentNode);
- set_backtracking(next);
- currentNode = currentNode->explore_child(next);
- this->action_trace->push_back(next);
+
+ nextThread = get_next_replay_thread();
+ curr->set_node(currentNode);
+ set_backtracking(curr);
+ currentNode = currentNode->explore_child(curr);
+ this->action_trace->push_back(curr);
}
void ModelChecker::print_summary(void)