this->scheduler = new Scheduler();
this->current_action = NULL;
+ this->exploring = NULL;
+ this->nextThread = THREAD_ID_T_NONE;
rootNode = new TreeNode(NULL);
currentNode = rootNode;
- action_trace = new std::list<class ModelAction *>();
+ action_trace = new action_list_t();
}
ModelChecker::~ModelChecker()
this->system_thread = t;
}
+Thread *ModelChecker::schedule_next_thread()
+{
+ Thread *t;
+ if (nextThread == THREAD_ID_T_NONE)
+ return NULL;
+ t = thread_map[nextThread];
+ if (t == NULL)
+ DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
+ return t;
+}
+
ModelAction *ModelChecker::get_last_conflict(ModelAction *act)
{
void *loc = act->get_location();
default:
break;
}
- std::list<class ModelAction *>::reverse_iterator rit;
+ action_list_t::reverse_iterator rit;
for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
ModelAction *prev = *rit;
if (prev->get_location() != loc)
prev->print();
act->print();
- /* FIXME */
- //Backtrack *back = new Backtrack(prev, actionList);
- //backtrackList->Append(back);
+ Backtrack *back = new Backtrack(prev, action_trace);
+ backtrack_list.push_back(back);
}
void ModelChecker::check_current_action(void)
void ModelChecker::print_trace(void)
{
- std::list<class ModelAction *>::iterator it;
+ action_list_t::iterator it;
printf("\n");
printf("---------------------------------------------------------------------\n");