model: utilize bad_synchronization flag
authorBrian Norris <banorris@uci.edu>
Mon, 1 Oct 2012 20:29:54 +0000 (13:29 -0700)
committerBrian Norris <banorris@uci.edu>
Mon, 1 Oct 2012 20:29:54 +0000 (13:29 -0700)
action.cc
model.cc

index 54ecce7..c744c65 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -228,7 +228,8 @@ void ModelAction::read_from(const ModelAction *act)
                rel_heads_list_t release_heads;
                model->get_release_seq_heads(this, &release_heads);
                for (unsigned int i = 0; i < release_heads.size(); i++)
                rel_heads_list_t release_heads;
                model->get_release_seq_heads(this, &release_heads);
                for (unsigned int i = 0; i < release_heads.size(); i++)
-                       synchronize_with(release_heads[i]);
+                       if (!synchronize_with(release_heads[i]))
+                               model->set_bad_synchronization();
        }
 }
 
        }
 }
 
index 9d2dbb6..47c6cdb 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1280,8 +1280,10 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                complete = release_seq_head(rf, &release_heads);
                for (unsigned int i = 0; i < release_heads.size(); i++) {
                        if (!act->has_synchronized_with(release_heads[i])) {
                complete = release_seq_head(rf, &release_heads);
                for (unsigned int i = 0; i < release_heads.size(); i++) {
                        if (!act->has_synchronized_with(release_heads[i])) {
-                               updated = true;
-                               act->synchronize_with(release_heads[i]);
+                               if (act->synchronize_with(release_heads[i]))
+                                       updated = true;
+                               else
+                                       set_bad_synchronization();
                        }
                }
 
                        }
                }