X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=9c0df20b5de89bd2876cde69ca281502506f4709;hb=3f77119600ac3aa246258dec2776056d09f8e4e0;hp=addf93f67469f1cd7f96a15ffad8ec5551cb1c1b;hpb=9aae08ba6d60aa253039d2da1c3571fdde2ac159;p=model-checker.git

diff --git a/nodestack.cc b/nodestack.cc
index addf93f..9c0df20 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -226,7 +226,7 @@ bool Node::misc_empty() const
  * @param value is the value to backtrack to.
  * @return True if the future value was successully added; false otherwise
  */
-bool Node::add_future_value(struct future_value& fv)
+bool Node::add_future_value(struct future_value fv)
 {
 	uint64_t value = fv.value;
 	modelclock_t expiration = fv.expiration;
@@ -348,6 +348,14 @@ thread_id_t Node::get_next_backtrack()
 	return int_to_id(i);
 }
 
+void Node::clear_backtracking()
+{
+	for (unsigned int i = 0; i < backtrack.size(); i++)
+		backtrack[i] = false;
+	for (unsigned int i = 0; i < explored_children.size(); i++)
+		explored_children[i] = false;
+}
+
 bool Node::is_enabled(Thread *t) const
 {
 	int thread_id = id_to_int(t->get_id());
@@ -556,7 +564,11 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena
 		if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow)
 			prevfairness = node_list[head_idx - model->params.fairwindow];
 	}
-	node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness));
+
+	int next_threads = model->get_num_threads();
+	if (act->get_type() == THREAD_CREATE)
+		next_threads++;
+	node_list.push_back(new Node(act, head, next_threads, prevfairness));
 	total_nodes++;
 	head_idx++;
 	return NULL;
@@ -577,6 +589,7 @@ void NodeStack::pop_restofstack(int numAhead)
 	for (unsigned int i = it; i < node_list.size(); i++)
 		delete node_list[i];
 	node_list.resize(it);
+	node_list.back()->clear_backtracking();
 }
 
 Node * NodeStack::get_head() const