ModelChecker::ModelChecker()
{
/* First thread created will have id INITIAL_THREAD_ID */
- this->next_thread_id = INITIAL_THREAD_ID;
+ next_thread_id = INITIAL_THREAD_ID;
used_sequence_numbers = 0;
/* Initialize default scheduler */
- this->scheduler = new Scheduler();
+ scheduler = new Scheduler();
num_executions = 0;
- this->current_action = NULL;
- this->exploring = NULL;
- this->nextThread = THREAD_ID_T_NONE;
+ current_action = NULL;
+ exploring = NULL;
+ nextThread = THREAD_ID_T_NONE;
rootNode = new TreeNode();
currentNode = rootNode;
free_action_list(action_trace);
- delete this->scheduler;
+ delete scheduler;
delete rootNode;
}
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");
if (prev == NULL)
return;
- node = prev->get_node();
+ node = prev->get_treenode();
while (t && !node->is_enabled(t))
t = t->get_parent();