}
ModelChecker::ModelChecker()
-{
- /* First thread created will have id INITIAL_THREAD_ID */
- this->next_thread_id = INITIAL_THREAD_ID;
- used_sequence_numbers = 0;
+ :
/* Initialize default scheduler */
- this->scheduler = new Scheduler();
-
- num_executions = 0;
- this->current_action = NULL;
- this->exploring = NULL;
- this->nextThread = THREAD_ID_T_NONE;
-
- rootNode = new TreeNode();
- currentNode = rootNode;
- action_trace = new action_list_t();
- global_vec = snapshot_utils::ReturnGlobalSegmentsToSnapshot();
+ scheduler(new Scheduler()),
+ /* First thread created will have id INITIAL_THREAD_ID */
+ next_thread_id(INITIAL_THREAD_ID),
+ used_sequence_numbers(0),
+
+ num_executions(0),
+ current_action(NULL),
+ exploring(NULL),
+ nextThread(THREAD_ID_T_NONE),
+ action_trace(new action_list_t()),
+ rootNode(new TreeNode()),
+ currentNode(rootNode)
+{
}
ModelChecker::~ModelChecker()
free_action_list(action_trace);
- delete this->scheduler;
+ delete scheduler;
delete rootNode;
}
current_action = NULL;
next_thread_id = INITIAL_THREAD_ID;
used_sequence_numbers = 0;
+ nextThread = 0;
/* scheduler reset ? */
}
ModelAction *next;
thread_id_t tid;
+ /* Have we completed exploring the preselected path? */
+ if (exploring == NULL)
+ return THREAD_ID_T_NONE;
+
+ /* Else, we are trying to replay an execution */
+ exploring->advance_state();
+
+ ASSERT(exploring->get_state() != NULL);
+
next = exploring->get_state();
if (next == exploring->get_diverge()) {
- TreeNode *node = next->get_node();
+ TreeNode *node = next->get_treenode();
/* Reached divergence point; discard our current 'exploring' */
DEBUG("*** Discard 'Backtrack' object ***\n");
return tid;
}
-thread_id_t ModelChecker::advance_backtracking_state()
-{
- /* Have we completed exploring the preselected path? */
- if (exploring == NULL)
- return THREAD_ID_T_NONE;
-
- /* Else, we are trying to replay an execution */
- exploring->advance_state();
-
- ASSERT(exploring->get_state() != NULL);
-
- return get_next_replay_thread();
-}
-
bool ModelChecker::next_execution()
{
DBG();
}
model->reset_to_initial_state();
- nextThread = get_next_replay_thread();
return true;
}
if (prev == NULL)
return;
- node = prev->get_node();
+ node = prev->get_treenode();
while (t && !node->is_enabled(t))
t = t->get_parent();
void ModelChecker::check_current_action(void)
{
- ModelAction *next = this->current_action;
-
- if (!next) {
+ ModelAction *curr = this->current_action;
+ current_action = NULL;
+ if (!curr) {
DEBUG("trying to push NULL action...\n");
return;
}
- current_action = NULL;
- nextThread = advance_backtracking_state();
- next->set_node(currentNode);
- set_backtracking(next);
- currentNode = currentNode->explore_child(next);
- this->action_trace->push_back(next);
+
+ nextThread = get_next_replay_thread();
+ curr->set_node(currentNode);
+ set_backtracking(curr);
+ currentNode = currentNode->explore_child(curr);
+ this->action_trace->push_back(curr);
}
void ModelChecker::print_summary(void)