+void ModelChecker::reset_to_initial_state()
+{
+ DEBUG("+++ Resetting to initial state +++\n");
+ std::map<thread_id_t, class Thread *>::iterator it;
+ for (it = thread_map.begin(); it != thread_map.end(); it++) {
+ delete (*it).second;
+ }
+ thread_map.clear();
+ action_trace = new action_list_t();
+ currentNode = rootNode;
+ current_action = NULL;
+ used_thread_id = INITIAL_THREAD_ID;
+ /* scheduler reset ? */
+}
+
+int ModelChecker::get_next_id()
+{
+ return ++used_thread_id;
+}
+
+Thread * ModelChecker::schedule_next_thread()
+{
+ Thread *t;
+ if (nextThread == THREAD_ID_T_NONE)
+ return NULL;
+ t = thread_map[nextThread];
+ if (t == NULL)
+ DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
+ return t;
+}
+
+/*
+ * get_next_replay_thread() - Choose the next thread in the replay sequence
+ *
+ * If we've reached the 'diverge' point, then we pick a thread from the
+ * backtracking set.
+ * Otherwise, we simply return the next thread in the sequence.
+ */
+thread_id_t ModelChecker::get_next_replay_thread()
+{
+ ModelAction *next;
+ thread_id_t tid;
+
+ next = exploring->get_state();
+
+ if (next == exploring->get_diverge()) {
+ TreeNode *node = next->get_node();
+
+ /* Reached divergence point; discard our current 'exploring' */
+ DEBUG("*** Discard 'Backtrack' object ***\n");
+ tid = node->getNextBacktrack();
+ delete exploring;
+ exploring = NULL;
+ } else {
+ tid = next->get_tid();
+ }
+ DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
+ 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();
+ if (exploring->get_state() == NULL)
+ DEBUG("*** error: reached end of backtrack trace\n");
+
+ return get_next_replay_thread();
+}
+
+bool ModelChecker::next_execution()
+{
+ num_executions++;
+ print_summary();
+ if ((exploring = model->get_next_backtrack()) == NULL)
+ return false;
+ model->reset_to_initial_state();
+ nextThread = get_next_replay_thread();
+ return true;
+}
+
+ModelAction * ModelChecker::get_last_conflict(ModelAction *act)