+ if (t == NULL) {
+ int old_curr_thread = curr_thread_index;
+ bool have_enabled_thread_with_priority = false;
+ Node *n = model->get_curr_node();
+
+ for (int i = 0; i < enabled_len; i++) {
+ thread_id_t tid = int_to_id(i);
+ if (n->has_priority(tid)) {
+ DEBUG("Node (tid %d) has priority\n", i);
+ //Have a thread with priority
+ if (enabled[i] != THREAD_DISABLED)
+ have_enabled_thread_with_priority = true;
+ }
+ }
+
+ while (true) {
+ curr_thread_index = (curr_thread_index + 1) % enabled_len;
+ thread_id_t curr_tid = int_to_id(curr_thread_index);
+ if (enabled[curr_thread_index] == THREAD_ENABLED &&
+ (!have_enabled_thread_with_priority || n->has_priority(curr_tid))) {
+ t = model->get_thread(curr_tid);
+ break;
+ }
+ if (curr_thread_index == old_curr_thread) {
+ if (DBG_ENABLED())
+ print();
+ return NULL;
+ }
+ }
+ } else if (t->is_model_thread()) {
+ /* model-checker threads never run */
+ ASSERT(false);
+ t = NULL;
+ } else {
+ curr_thread_index = id_to_int(t->get_id());
+ }
+
+ current = t;
+ if (DBG_ENABLED())
+ print();
+ return t;
+}
+
+/**
+ * @return The currently-running Thread
+ */
+Thread * Scheduler::get_current_thread() const
+{
+ ASSERT(!current || !current->is_model_thread());