X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=nodestack.cc;h=74e6a11a43bbeacab4cc0e3dc39a9ee0dc279760;hb=bac91bab68e2a50aa5ceee4057624a56eaf6c9bf;hp=379fb3b1fc15f219cdd870b4976af0e394fd2263;hpb=810306cb85accaaace9a50f174264f105991230b;p=model-checker.git

diff --git a/nodestack.cc b/nodestack.cc
index 379fb3b..74e6a11 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -1,21 +1,14 @@
 #include "nodestack.h"
 #include "action.h"
 #include "common.h"
+#include "model.h"
 
-int Node::total_nodes = 0;
-
-Node::Node(ModelAction *act, Node *parent)
+Node::Node(ModelAction *act, int nthreads)
 	: action(act),
-	num_threads(parent ? parent->num_threads : 1),
+	num_threads(nthreads),
 	explored_children(num_threads),
 	backtrack(num_threads)
 {
-	total_nodes++;
-	if (act && act->get_type() == THREAD_CREATE) {
-		num_threads++;
-		explored_children.resize(num_threads);
-		backtrack.resize(num_threads);
-	}
 }
 
 Node::~Node()
@@ -98,8 +91,10 @@ static void clear_node_list(node_list_t *list, node_list_t::iterator start,
 }
 
 NodeStack::NodeStack()
+	: total_nodes(0)
 {
 	node_list.push_back(new Node());
+	total_nodes++;
 	iter = node_list.begin();
 }
 
@@ -139,7 +134,8 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 
 		/* Record action */
 		get_head()->explore_child(act);
-		node_list.push_back(new Node(act, get_head()));
+		node_list.push_back(new Node(act, model->get_num_threads()));
+		total_nodes++;
 		iter++;
 	}
 	return (*iter)->get_action();