/* Initialize default scheduler */
this->scheduler = new Scheduler();
+ num_executions = 0;
this->current_action = NULL;
this->exploring = NULL;
this->nextThread = THREAD_ID_T_NONE;
this->system_thread = t;
}
-Thread *ModelChecker::schedule_next_thread()
+Thread * ModelChecker::schedule_next_thread()
{
Thread *t;
if (nextThread == THREAD_ID_T_NONE)
return get_next_replay_thread();
}
-ModelAction *ModelChecker::get_last_conflict(ModelAction *act)
+bool ModelChecker::next_execution()
+{
+ num_executions++;
+ if ((exploring = model->get_next_backtrack()) == NULL)
+ return false;
+ model->reset_to_initial_state();
+ nextThread = get_next_replay_thread();
+ return true;
+}
+
+ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
{
void *loc = act->get_location();
action_type type = act->get_type();
default:
break;
}
+ /* linear search: from most recent to oldest */
action_list_t::reverse_iterator rit;
for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
ModelAction *prev = *rit;
printf("\n");
printf("---------------------------------------------------------------------\n");
+ printf("Number of executions: %d\n", num_executions);
printf("Total nodes created: %d\n\n", TreeNode::getTotalNodes());
+ scheduler->print();
+
+ printf("\nTrace:\n\n");
+
for (it = action_trace->begin(); it != action_trace->end(); it++) {
DBG();
(*it)->print();