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 e4d3016e0eeaa9cfdec58d5c57f4cf0ba2dadbe8..19d273de50bf67aa60cf6835845b21ac347fc7be 100644 (file)
--- 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 */