From: Brian Norris <banorris@uci.edu>
Date: Wed, 18 Apr 2012 00:50:29 +0000 (-0700)
Subject: tree: add class TreeNode
X-Git-Tag: pldi2013~549
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c5bccfe70ac59fc1b6c32708805be22519e1a6ba;p=model-checker.git

tree: add class TreeNode

Untested, but ported from Nachos project.
---

diff --git a/Makefile b/Makefile
index f484bb9..d134f02 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 CC=g++
 BIN=model
-SOURCE=libthreads.cc schedule.cc libatomic.cc userprog.c model.cc malloc.c threads.cc
-HEADERS=libthreads.h schedule.h common.h libatomic.h model.h threads.h
+SOURCE=libthreads.cc schedule.cc libatomic.cc userprog.c model.cc malloc.c threads.cc tree.cc
+HEADERS=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h
 FLAGS=-Wall -ldl -g
 
 all: ${BIN}
diff --git a/tree.cc b/tree.cc
new file mode 100644
index 0000000..37dfa26
--- /dev/null
+++ b/tree.cc
@@ -0,0 +1,56 @@
+#include "tree.h"
+
+int TreeNode::totalNodes = 0;
+
+TreeNode::TreeNode(TreeNode *par)
+{
+	TreeNode::totalNodes++;
+	this->parent = par;
+}
+
+TreeNode::~TreeNode() {
+	std::map<tree_t, class TreeNode *>::iterator it;
+
+	for (it = children.begin(); it != children.end(); it++)
+		delete it->second;
+	delete &children;
+}
+
+TreeNode *TreeNode::exploreChild(tree_t id)
+{
+	TreeNode *n;
+	std::set<tree_t >::iterator it;
+
+	if (!hasBeenExplored(id)) {
+		n = new TreeNode(this);
+		children[id] = n;
+	} else {
+		n = children[id];
+	}
+	if ((it = backtrack.find(id)) != backtrack.end())
+		backtrack.erase(it);
+
+	return n;
+}
+
+int TreeNode::setBacktrack(tree_t id)
+{
+	if (backtrack.find(id) == backtrack.end())
+		return 1;
+	backtrack.insert(id);
+	return 0;
+}
+
+tree_t TreeNode::getNextBacktrack()
+{
+	if (backtrack.empty())
+		return NULL;
+	return *backtrack.begin();
+}
+
+TreeNode *TreeNode::getRoot()
+{
+	if (parent)
+		return parent->getRoot();
+	return this;
+}
diff --git a/tree.h b/tree.h
new file mode 100644
index 0000000..766aacd
--- /dev/null
+++ b/tree.h
@@ -0,0 +1,30 @@
+#include <set>
+#include <map>
+#include "threads.h"
+
+typedef thread_id_t tree_t;
+
+/*
+ * An n-ary tree
+ *
+ * A tree with n possible branches from each node - used for recording the
+ * execution paths we've executed / backtracked
+ */
+class TreeNode {
+public:
+	TreeNode(TreeNode *par);
+	~TreeNode();
+	bool hasBeenExplored(tree_t id) { return children.find(id) != children.end(); }
+	TreeNode *exploreChild(tree_t id);
+	tree_t getNextBacktrack();
+
+	/* Return 1 if already in backtrack, 0 otherwise */
+	int setBacktrack(tree_t id);
+	TreeNode *getRoot();
+	static int getTotalNodes() { return TreeNode::totalNodes; }
+private:
+	TreeNode *parent;
+	std::map<tree_t, class TreeNode *> children;
+	std::set<tree_t> backtrack;
+	static int totalNodes;
+};