X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=4da3cd60fd7db93c147fba60faf929d6fccb9a0f;hb=fc32611957cecd106751b62bc4de4aeddc9af56c;hp=f73d4cf4a154e264ed93a32f250c6a0f6dfaa11a;hpb=5d5b4d719178c48c3e5f616b5eb61b7d68dc2b49;p=model-checker.git

diff --git a/nodestack.cc b/nodestack.cc
index f73d4cf..4da3cd6 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -91,7 +91,7 @@ void Node::print()
 	if (action)
 		action->print();
 	else
-		printf("******** empty action ********\n");
+		model_print("******** empty action ********\n");
 }
 
 /** @brief Prints info about may_read_from set */
@@ -193,30 +193,33 @@ bool Node::misc_empty() {
 
 /**
  * Adds a value from a weakly ordered future write to backtrack to. This
- * operation may "fail" if the future value is already set (with a later
- * expiration), or if the futurevalues set has reached its maximum.
+ * operation may "fail" if the future value has already been run (within some
+ * sloppiness window of this expiration), or if the futurevalues set has
+ * reached its maximum.
  * @see model_params.maxfuturevalues
  *
  * @param value is the value to backtrack to.
  * @return True if the future value was successully added; false otherwise
  */
 bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
-	int suitableindex=-1;
+	int idx = -1; /* Highest index where value is found */
 	for (unsigned int i = 0; i < future_values.size(); i++) {
 		if (future_values[i].value == value) {
-			if (future_values[i].expiration>=expiration)
+			if (expiration <= future_values[i].expiration)
 				return false;
-			if (future_index < ((int) i)) {
-				suitableindex=i;
-			}
+			idx = i;
 		}
 	}
-
-	if (suitableindex!=-1) {
-		future_values[suitableindex].expiration=expiration;
+	if (idx > future_index) {
+		/* Future value hasn't been explored; update expiration */
+		future_values[idx].expiration = expiration;
 		return true;
+	} else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
+		/* Future value has been explored and is within the "sloppy" window */
+		return false;
 	}
 
+	/* Limit the size of the future-values set */
 	if (model->params.maxfuturevalues > 0 &&
 			(int)future_values.size() >= model->params.maxfuturevalues)
 		return false;
@@ -492,14 +495,14 @@ NodeStack::~NodeStack()
 
 void NodeStack::print()
 {
-	printf("............................................\n");
-	printf("NodeStack printing node_list:\n");
+	model_print("............................................\n");
+	model_print("NodeStack printing node_list:\n");
 	for (unsigned int it = 0; it < node_list.size(); it++) {
 		if (it == this->iter)
-			printf("vvv following action is the current iterator vvv\n");
+			model_print("vvv following action is the current iterator vvv\n");
 		node_list[it]->print();
 	}
-	printf("............................................\n");
+	model_print("............................................\n");
 }
 
 /** Note: The is_enabled set contains what actions were enabled when