+/**
+ * Performs the "scheduling" for the model-checker. That is, it checks if the
+ * model-checker has selected a "next thread to run" and returns it, if
+ * available. This function should be called from the Scheduler routine, where
+ * the Scheduler falls back to a default scheduling routine if needed.
+ *
+ * @return The next thread chosen by the model-checker. If the model-checker
+ * makes no selection, retuns NULL.
+ */
+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;
+}
+
+/**
+ * Choose the next thread in the replay sequence.
+ *
+ * If the replay sequence has reached the 'diverge' point, returns a thread
+ * from the backtracking set. Otherwise, simply returns the next thread in the
+ * sequence that is being replayed.
+ */
+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()->get_parent();
+
+ /* 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;
+}
+
+/**
+ * Queries the model-checker for more executions to explore and, if one
+ * exists, resets the model-checker state to execute a new execution.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
+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)