+ std::map<int, class Thread *>::iterator it;
+ for (it = thread_map->begin(); it != thread_map->end(); it++)
+ delete (*it).second;
+ delete thread_map;
+
+ delete action_trace;
+
+ delete node_stack;
+ delete scheduler;
+}
+
+void ModelChecker::reset_to_initial_state()
+{
+ DEBUG("+++ Resetting to initial state +++\n");
+ node_stack->reset_execution();
+ current_action = NULL;
+ next_thread_id = INITIAL_THREAD_ID;
+ used_sequence_numbers = 0;
+ nextThread = 0;
+ next_backtrack = NULL;
+ snapshotObject->backTrackBeforeStep(0);
+}
+
+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;
+}
+
+Thread * ModelChecker::schedule_next_thread()
+{
+ Thread *t;
+ if (nextThread == THREAD_ID_T_NONE)
+ return NULL;
+ t = (*thread_map)[id_to_int(nextThread)];
+
+ ASSERT(t != NULL);
+
+ 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;
+
+ /* Have we completed exploring the preselected path? */
+ if (diverge == NULL)
+ return THREAD_ID_T_NONE;
+
+ /* Else, we are trying to replay an execution */
+ next = node_stack->get_next()->get_action();
+
+ if (next == diverge) {
+ Node *node = next->get_node();
+
+ /* Reached divergence point */
+ DEBUG("*** Divergence point ***\n");
+ tid = node->get_next_backtrack();
+ diverge = NULL;
+ } else {
+ tid = next->get_tid();
+ }
+ DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
+ return tid;
+}
+
+bool ModelChecker::next_execution()
+{
+ DBG();
+
+ num_executions++;
+ print_summary();
+ if ((diverge = model->get_next_backtrack()) == NULL)
+ return false;
+
+ if (DBG_ENABLED()) {
+ printf("Next execution will diverge at:\n");
+ diverge->print();
+ }
+
+ model->reset_to_initial_state();
+ return true;
+}
+
+ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
+{
+ action_type type = act->get_type();
+
+ switch (type) {
+ case THREAD_CREATE:
+ case THREAD_YIELD:
+ case THREAD_JOIN:
+ return NULL;
+ case ATOMIC_READ:
+ case ATOMIC_WRITE:
+ default:
+ break;
+ }
+ /* linear search: from most recent to oldest */
+ action_list_t::reverse_iterator rit;
+ for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (act->is_dependent(prev))
+ return prev;
+ }
+ return NULL;