From: Brian Norris <banorris@uci.edu>
Date: Mon, 25 Jun 2012 18:47:24 +0000 (-0700)
Subject: nodestack: add Node::get_parent() function
X-Git-Tag: pldi2013~389^2^2~6
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=2fd874e12b6349b5543b9a3014b38b556c672623;p=model-checker.git

nodestack: add Node::get_parent() function

As I add more complicated backtracking and may-read-from relationships,
each Node might need some structural information to be able to reach its
parent Node.

To support this:
* the NodeStack should provide the parent information via Node constructor
* the Node should provide a get_parent() method
---

diff --git a/nodestack.cc b/nodestack.cc
index 87b3ee5..e7b5f51 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -4,8 +4,9 @@
 #include "model.h"
 
 /** @brief Node constructor */
-Node::Node(ModelAction *act, int nthreads)
+Node::Node(ModelAction *act, Node *par, int nthreads)
 	: action(act),
+	parent(par),
 	num_threads(nthreads),
 	explored_children(num_threads),
 	backtrack(num_threads),
@@ -173,7 +174,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
 
 	/* Record action */
 	get_head()->explore_child(act);
-	node_list.push_back(new Node(act, model->get_num_threads()));
+	node_list.push_back(new Node(act, get_head(), model->get_num_threads()));
 	total_nodes++;
 	iter++;
 	return NULL;
diff --git a/nodestack.h b/nodestack.h
index 74ac245..11440e5 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -18,7 +18,7 @@ typedef std::set< ModelAction *, std::less< ModelAction *>, MyAlloc< ModelAction
 
 class Node {
 public:
-	Node(ModelAction *act = NULL, int nthreads = 1);
+	Node(ModelAction *act = NULL, Node *par = NULL, int nthreads = 1);
 	~Node();
 	/* return true = thread choice has already been explored */
 	bool has_been_explored(thread_id_t tid);
@@ -31,6 +31,10 @@ public:
 	bool is_enabled(Thread *t);
 	ModelAction * get_action() { return action; }
 
+	/** @return the parent Node to this Node; that is, the action that
+	 * occurred previously in the stack. */
+	Node * get_parent() const { return parent; }
+
 	void add_read_from(ModelAction *act);
 
 	void print();
@@ -40,6 +44,7 @@ private:
 	void explore(thread_id_t tid);
 
 	ModelAction *action;
+	Node *parent;
 	int num_threads;
 	std::vector< bool, MyAlloc<bool> > explored_children;
 	std::vector< bool, MyAlloc<bool> > backtrack;