From 38dfa065a8c9404427bcd954b37cf343aa4f9ea8 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 28 Mar 2013 15:27:17 -0700
Subject: [PATCH] nodestack: move "behaviors" increment all into Node wrapper
 function

---
 model.cc     | 16 ++--------------
 nodestack.cc | 21 +++++++++++++++++++++
 nodestack.h  |  2 ++
 3 files changed, 25 insertions(+), 14 deletions(-)

diff --git a/model.cc b/model.cc
index 879f1de..0423c6e 100644
--- a/model.cc
+++ b/model.cc
@@ -260,20 +260,8 @@ Thread * ModelChecker::get_next_thread()
 		scheduler->update_sleep_set(prevnode);
 
 		/* Reached divergence point */
-		if (nextnode->increment_misc()) {
-			/* The next node will try to satisfy a different misc_index values. */
-			tid = next->get_tid();
-			node_stack->pop_restofstack(2);
-		} else if (nextnode->increment_promise()) {
-			/* The next node will try to satisfy a different set of promises. */
-			tid = next->get_tid();
-			node_stack->pop_restofstack(2);
-		} else if (nextnode->increment_read_from()) {
-			/* The next node will read from a different value. */
-			tid = next->get_tid();
-			node_stack->pop_restofstack(2);
-		} else if (nextnode->increment_relseq_break()) {
-			/* The next node will try to resolve a release sequence differently */
+		if (nextnode->increment_behaviors()) {
+			/* Execute the same thread with a new behavior */
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
 		} else {
diff --git a/nodestack.cc b/nodestack.cc
index 2fa8784..f46e4b7 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -726,6 +726,27 @@ bool Node::relseq_break_empty() const
 
 /******************* end breaking release sequences ***************************/
 
+/**
+ * Increments some behavior's index, if a new behavior is available
+ * @return True if there is a new behavior available; otherwise false
+ */
+bool Node::increment_behaviors()
+{
+	/* satisfy a different misc_index values */
+	if (increment_misc())
+		return true;
+	/* satisfy a different set of promises */
+	if (increment_promise())
+		return true;
+	/* read from a different value */
+	if (increment_read_from())
+		return true;
+	/* resolve a release sequence differently */
+	if (increment_relseq_break())
+		return true;
+	return false;
+}
+
 NodeStack::NodeStack() :
 	node_list(),
 	head_idx(-1),
diff --git a/nodestack.h b/nodestack.h
index 99374a3..8573e9f 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -112,6 +112,8 @@ public:
 	bool increment_relseq_break();
 	bool relseq_break_empty() const;
 
+	bool increment_behaviors();
+
 	void print() const;
 
 	MEMALLOC
-- 
2.34.1