+ return dequeue_thread();
+}
+
+void scheduler_init(struct model_checker *mod)
+{
+ struct scheduler *sched;
+
+ /* Initialize FCFS scheduler */
+ sched = malloc(sizeof(*sched));
+ sched->init = NULL;
+ sched->exit = NULL;
+ sched->add_thread = schedule_add_thread;
+ sched->next_thread = schedule_choose_next;
+ sched->get_current_thread = thread_current;
+ mod->scheduler = sched;