From: Brian Norris <banorris@uci.edu>
Date: Thu, 21 Jun 2012 09:04:11 +0000 (-0700)
Subject: model: build up 'may_read_from' set
X-Git-Tag: pldi2013~391^2~3
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=236f53b4a7b4c07e9f60b662e059838f75b24171;p=model-checker.git

model: build up 'may_read_from' set

Finally wire up the model-checker so that it builds the may_read_from set
for every 'read' action. I think this is working OK, although I don't have
much to really test it on yet.

Also, improve comments to describe the process in check_current_action().
---

diff --git a/model.cc b/model.cc
index e4d3016..19d273d 100644
--- a/model.cc
+++ b/model.cc
@@ -240,11 +240,18 @@ void ModelChecker::check_current_action(void)
 
 	tmp = node_stack->explore_action(curr);
 	if (tmp) {
-		/* Discard duplicate ModelAction */
+		/* Discard duplicate ModelAction; use action from NodeStack */
 		delete curr;
 		curr = tmp;
 	} else {
+		/*
+		 * Perform one-time actions when pushing new ModelAction onto
+		 * NodeStack
+		 */
 		curr->create_cv(get_parent_action(curr->get_tid()));
+		/* Build may_read_from set */
+		if (curr->is_read())
+			build_reads_from_past(curr);
 	}
 
 	/* Assign 'creation' parent */