Simply use the hollow 'check_current_action()' interface to perform model
checking in the thread_system_next() call.
Right now, this just adds the previous (a.k.a. 'current') action to our log.
struct thread *curr, *next;
curr = thread_current();
struct thread *curr, *next;
curr = thread_current();
+ model->check_current_action();
if (curr) {
if (curr->state == THREAD_READY)
model->scheduler->add_thread(curr);
if (curr) {
if (curr->state == THREAD_READY)
model->scheduler->add_thread(curr);