model: always re-calculate clock vectors
authorBrian Norris <banorris@uci.edu>
Tue, 2 Oct 2012 00:20:34 +0000 (17:20 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 2 Oct 2012 00:40:17 +0000 (17:40 -0700)
Clock vectors are mutable, via synchronization. We will need to both
snapshot and recompute clock vectors as they are generated. Right now,
we have some incorrect assumptions in place. This bugfix prevents stale
clock vectors (from previous executions) from polluting subsequent
executions.

model.cc

index 468900a..c4bc693 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -543,10 +543,7 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                /* Discard duplicate ModelAction; use action from NodeStack */
                delete curr;
 
                /* Discard duplicate ModelAction; use action from NodeStack */
                delete curr;
 
-               /* If we have diverged, we need to reset the clock vector. */
-               if (diverge == NULL) {
-                       newcurr->create_cv(get_parent_action(newcurr->get_tid()));
-               }
+               newcurr->create_cv(get_parent_action(newcurr->get_tid()));
        } else {
                newcurr = curr;
                /*
        } else {
                newcurr = curr;
                /*