From: Brian Norris <banorris@uci.edu>
Date: Fri, 4 May 2012 06:27:46 +0000 (-0700)
Subject: tree: revise arguments (use Thread, ModelAction)
X-Git-Tag: pldi2013~458
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=6b3cc5b800966b58d330bf516d92a17b4e2bee9d;p=model-checker.git

tree: revise arguments (use Thread, ModelAction)

Preparation for other changes to the TreeNode.
---

diff --git a/model.cc b/model.cc
index aba3e8b..0084e74 100644
--- a/model.cc
+++ b/model.cc
@@ -43,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();
 }
@@ -182,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)
@@ -190,14 +191,14 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	node = prev->get_node();
 
 	/* 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();
@@ -229,7 +230,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);
 }
 
diff --git a/tree.cc b/tree.cc
index ce79f75..57e0c13 100644
--- a/tree.cc
+++ b/tree.cc
@@ -1,8 +1,9 @@
 #include "tree.h"
+#include "action.h"
 
 int TreeNode::totalNodes = 0;
 
-TreeNode::TreeNode(TreeNode *par)
+TreeNode::TreeNode(TreeNode *par, ModelAction *act)
 {
 	TreeNode::totalNodes++;
 	this->parent = par;
@@ -15,14 +16,15 @@ TreeNode::~TreeNode() {
 		delete it->second;
 }
 
-TreeNode * TreeNode::exploreChild(thread_id_t id)
+TreeNode * TreeNode::explore_child(ModelAction *act)
 {
 	TreeNode *n;
 	std::set<int>::iterator it;
+	thread_id_t id = act->get_tid();
 	int i = id_to_int(id);
 
 	if (!hasBeenExplored(id)) {
-		n = new TreeNode(this);
+		n = new TreeNode(this, act);
 		children[i] = n;
 	} else {
 		n = children[i];
diff --git a/tree.h b/tree.h
index 9fba203..1752d3f 100644
--- a/tree.h
+++ b/tree.h
@@ -5,6 +5,8 @@
 #include <map>
 #include "threads.h"
 
+class ModelAction;
+
 /*
  * An n-ary tree
  *
@@ -13,10 +15,10 @@
  */
 class TreeNode {
 public:
-	TreeNode(TreeNode *par);
+	TreeNode(TreeNode *par = NULL, ModelAction *act = NULL);
 	~TreeNode();
 	bool hasBeenExplored(thread_id_t id) { return children.find(id_to_int(id)) != children.end(); }
-	TreeNode * exploreChild(thread_id_t id);
+	TreeNode * explore_child(ModelAction *act);
 	thread_id_t getNextBacktrack();
 
 	/* Return 1 if already in backtrack, 0 otherwise */