From: Brian Norris <banorris@uci.edu>
Date: Wed, 22 Aug 2012 23:45:55 +0000 (-0700)
Subject: nodestack: turn magic promise numbers into enum + typedef
X-Git-Tag: pldi2013~257
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=379bbd92e88f756e39883dbac98c68b1d0699a66

nodestack: turn magic promise numbers into enum + typedef

Document the enum properly, since it's quite unclear what these flags really
mean.
---

diff --git a/nodestack.cc b/nodestack.cc
index 5c54475..2ebfc71 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -62,8 +62,8 @@ void Node::print_may_read_from()
  */
 void Node::set_promise(unsigned int i) {
 	if (i >= promises.size())
-		promises.resize(i + 1, 0);
-	promises[i] = 1;
+		promises.resize(i + 1, PROMISE_IGNORE);
+	promises[i] = PROMISE_UNFULFILLED;
 }
 
 /**
@@ -72,7 +72,7 @@ void Node::set_promise(unsigned int i) {
  * @return true if the promise should be satisfied by the given model action.
  */
 bool Node::get_promise(unsigned int i) {
-	return (i < promises.size()) && (promises[i] == 2);
+	return (i < promises.size()) && (promises[i] == PROMISE_FULFILLED);
 }
 
 /**
@@ -81,12 +81,12 @@ bool Node::get_promise(unsigned int i) {
  */
 bool Node::increment_promise() {
 	for (unsigned int i = 0; i < promises.size(); i++) {
-		if (promises[i] == 1) {
-			promises[i] = 2;
+		if (promises[i] == PROMISE_UNFULFILLED) {
+			promises[i] = PROMISE_FULFILLED;
 			while (i > 0) {
 				i--;
-				if (promises[i] == 2)
-					promises[i] = 1;
+				if (promises[i] == PROMISE_FULFILLED)
+					promises[i] = PROMISE_UNFULFILLED;
 			}
 			return true;
 		}
@@ -100,7 +100,7 @@ bool Node::increment_promise() {
  */
 bool Node::promise_empty() {
 	for (unsigned int i = 0; i < promises.size();i++)
-		if (promises[i] == 1)
+		if (promises[i] == PROMISE_UNFULFILLED)
 			return false;
 	return true;
 }
diff --git a/nodestack.h b/nodestack.h
index 6860467..b440b11 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -13,6 +13,19 @@
 
 class ModelAction;
 
+/**
+ * A flag used for the promise counting/combination problem within a node,
+ * denoting whether a particular Promise is
+ * <ol><li>@b applicable: can be satisfied by this Node's ModelAction and</li>
+ * <li>@b fulfilled: satisfied by this Node's ModelAction under the current
+ * configuration.</li></ol>
+ */
+typedef enum {
+	PROMISE_IGNORE = 0, /**< This promise is inapplicable; ignore it */
+	PROMISE_UNFULFILLED, /**< This promise is applicable but unfulfilled */
+	PROMISE_FULFILLED /**< This promise is applicable and fulfilled */
+} promise_t;
+
 /**
  * @brief A single node in a NodeStack
  *
@@ -78,7 +91,7 @@ private:
 	unsigned int read_from_index;
 
 	std::vector< uint64_t, MyAlloc< uint64_t > > future_values;
-	std::vector< unsigned int, MyAlloc<unsigned int> > promises;
+	std::vector< promise_t, MyAlloc<promise_t> > promises;
 	unsigned int future_index;
 };