this->scheduler = new Scheduler();
this->current_action = NULL;
+ this->exploring = NULL;
+ this->nextThread = THREAD_ID_T_NONE;
rootNode = new TreeNode(NULL);
currentNode = rootNode;
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();
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)