X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=tree.cc;h=c161ca838de4947fbfc1ca486aaaf0400ca1475e;hb=ab287cbc807422f31a4626cd755378b72e9294b3;hp=ce79f755eeea010897bc117f47deab11bb53786e;hpb=9f1c792a01ecbc86624f4c16d0a2bc763485a590;p=model-checker.git

diff --git a/tree.cc b/tree.cc
index ce79f75..c161ca8 100644
--- a/tree.cc
+++ b/tree.cc
@@ -1,11 +1,19 @@
 #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;
+	if (!parent) {
+		num_threads = 1;
+	} else {
+		num_threads = parent->num_threads;
+		if (act && act->get_type() == THREAD_CREATE)
+			num_threads++;
+	}
 }
 
 TreeNode::~TreeNode() {
@@ -15,14 +23,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];
@@ -55,3 +64,8 @@ TreeNode * TreeNode::getRoot()
 		return parent->getRoot();
 	return this;
 }
+
+bool TreeNode::is_enabled(Thread *t)
+{
+	return id_to_int(t->get_id()) < num_threads;
+}