- }
-}
-
-void ModelChecker::handleChosenThread(Thread *old)
-{
- if (execution->has_asserted())
- finishRunExecution(old);
- if (!chosen_thread)
- chosen_thread = get_next_thread();
- if (!chosen_thread || chosen_thread->is_model_thread())
- finishRunExecution(old);
- if (chosen_thread->just_woken_up()) {
- chosen_thread->set_wakeup_state(false);
- chosen_thread->set_pending(NULL);
- chosen_thread = NULL;
- // Allow this thread to stash the next pending action
- if (should_terminate_execution())
- finishRunExecution(old);
- else
- continueRunExecution(old);
- } else {
- /* Consume the next action for a Thread */
- consumeAction();
-
- if (should_terminate_execution())
- finishRunExecution(old);
- else
- continueRunExecution(old);