+ /* No thread was enabled */
+ return NULL;
+}
+
+void Scheduler::set_scheduler_thread(thread_id_t tid) {
+ curr_thread_index=id_to_int(tid);
+}
+
+/**
+ * @brief Set the current "running" Thread
+ * @param t Thread to run
+ */
+void Scheduler::set_current_thread(Thread *t)
+{
+ ASSERT(t && !t->is_model_thread());
+
+ // curr_thread_index = id_to_int(t->get_id());