#include "snapshot-interface.h"
/**
- * The thread_system_next function takes the next step in the execution.
- * @return Returns the 1 if there is another step and 0 otherwise.
+ * The thread_system_next function takes the next step in the execution, if
+ * possible.
+ * @return Returns 0 (success) if there is another step and non-zero otherwise.
*/
static int thread_system_next(void) {
Thread *curr, *next;
if (curr->get_state() == THREAD_READY) {
model->check_current_action();
model->scheduler->add_thread(curr);
- } else if (curr->get_state() == THREAD_RUNNING)
+ } else if (curr->get_state() == THREAD_RUNNING) {
/* Stopped while running; i.e., completed */
curr->complete();
- else
+ } else {
ASSERT(false);
+ }
}
next = model->scheduler->next_thread();
+
+ /* Infeasible -> don't take any more steps */
if (!model->isfeasible())
return 1;
+
if (next)
next->set_state(THREAD_RUNNING);
DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+
+ /* next == NULL -> don't take any more steps */
if (!next)
return 1;
+ /* Return non-zero only if swap fails with an error */
return Thread::swap(model->get_system_context(), next);
}