exit_flag(false),
scheduler(new Scheduler()),
node_stack(new NodeStack()),
- execution(new ModelExecution(this, &this->params, scheduler, node_stack)), // L: Model thread is created inside
+ execution(new ModelExecution(this, &this->params, scheduler, node_stack)),
execution_number(1),
diverge(NULL),
earliest_diverge(NULL),
return scheduler->select_next_thread(node_stack->get_head());
}
-/**
- * We need to know what the next actions of all threads in the sleep
- * set will be. This method computes them and stores the actions at
- * the corresponding thread object's pending action.
- */
-void ModelChecker::execute_sleep_set()
-{
- for (unsigned int i = 0; i < get_num_threads(); i++) {
- thread_id_t tid = int_to_id(i);
- Thread *thr = get_thread(tid);
- if (scheduler->is_sleep_set(thr) && thr->get_pending()) {
- thr->get_pending()->set_sleep_flag();
- }
- }
-}
-
/**
* @brief Assert a bug in the executing program.
*