X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=e3238258a3aa86b0570ff8ed8159eb62e27a899c;hb=c5e14aa2426f21f8de620cf24ed321447d75c989;hp=976b395db7889a123465d6ba89533503aa99a749;hpb=5b77072388b791acaa97ba4b01a0bdb85b21975e;p=model-checker.git

diff --git a/model.cc b/model.cc
index 976b395..e323825 100644
--- a/model.cc
+++ b/model.cc
@@ -8,6 +8,26 @@
 
 #define INITIAL_THREAD_ID	0
 
+class Backtrack {
+public:
+	Backtrack(ModelAction *d, action_list_t *t) {
+		diverge = d;
+		actionTrace = t;
+		iter = actionTrace->begin();
+	}
+	ModelAction * get_diverge() { return diverge; }
+	action_list_t * get_trace() { return actionTrace; }
+	void advance_state() { iter++; }
+	ModelAction * get_state() {
+		return iter == actionTrace->end() ? NULL : *iter;
+	}
+private:
+	ModelAction *diverge;
+	action_list_t *actionTrace;
+	/* points to position in actionTrace as we replay */
+	action_list_t::iterator iter;
+};
+
 ModelChecker *model;
 
 ModelChecker::ModelChecker()
@@ -23,7 +43,7 @@ ModelChecker::ModelChecker()
 	this->exploring = NULL;
 	this->nextThread = THREAD_ID_T_NONE;
 
-	rootNode = new TreeNode(NULL);
+	rootNode = new TreeNode();
 	currentNode = rootNode;
 	action_trace = new action_list_t();
 }
@@ -108,18 +128,27 @@ thread_id_t ModelChecker::advance_backtracking_state()
 
 	/* Else, we are trying to replay an execution */
 	exploring->advance_state();
-	if (exploring->get_state() == NULL)
-		DEBUG("*** error: reached end of backtrack trace\n");
+
+	ASSERT(exploring->get_state() != NULL);
 
 	return get_next_replay_thread();
 }
 
 bool ModelChecker::next_execution()
 {
+	DBG();
+
 	num_executions++;
 	print_summary();
 	if ((exploring = model->get_next_backtrack()) == NULL)
 		return false;
+
+	if (DBG_ENABLED()) {
+		printf("Next execution will diverge at:\n");
+		exploring->get_diverge()->print();
+		print_list(exploring->get_trace());
+	}
+
 	model->reset_to_initial_state();
 	nextThread = get_next_replay_thread();
 	return true;
@@ -153,6 +182,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 {
 	ModelAction *prev;
 	TreeNode *node;
+	Thread *t = get_thread(act->get_tid());
 
 	prev = get_last_conflict(act);
 	if (prev == NULL)
@@ -160,15 +190,18 @@ void ModelChecker::set_backtracking(ModelAction *act)
 
 	node = prev->get_node();
 
+	while (t && !node->is_enabled(t))
+		t = t->get_parent();
+
 	/* Check if this has been explored already */
-	if (node->hasBeenExplored(act->get_tid()))
+	if (node->hasBeenExplored(t->get_id()))
 		return;
 	/* If this is a new backtracking point, mark the tree */
-	if (node->setBacktrack(act->get_tid()) != 0)
+	if (node->setBacktrack(t->get_id()) != 0)
 		return;
 
 	DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
-			prev->get_tid(), act->get_tid());
+			prev->get_tid(), t->get_id());
 	if (DBG_ENABLED()) {
 		prev->print();
 		act->print();
@@ -200,7 +233,7 @@ void ModelChecker::check_current_action(void)
 	nextThread = advance_backtracking_state();
 	next->set_node(currentNode);
 	set_backtracking(next);
-	currentNode = currentNode->exploreChild(next->get_tid());
+	currentNode = currentNode->explore_child(next);
 	this->action_trace->push_back(next);
 }