#include "model.h"
#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.
+ * @return Returns the 1 if there is another step and 0 otherwise.
*/
-
static int thread_system_next(void) {
Thread *curr, *next;
ASSERT(false);
}
next = model->scheduler->next_thread();
+ 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);
/** The thread_wait_finish method runs the current execution until we
* have no more steps to take.
*/
-
static void thread_wait_finish(void) {
DBG();
/** The real_main function contains the main model checking loop. */
-
-void real_main() {
+static void real_main() {
thrd_t user_thread;
ucontext_t main_context;
model->set_system_context(&main_context);
snapshotObject->snapshotStep(0);
-
do {
/* Start user program */
model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));