projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
939c3e1
)
model: utilize bad_synchronization flag
author
Brian Norris
<banorris@uci.edu>
Mon, 1 Oct 2012 20:29:54 +0000
(13:29 -0700)
committer
Brian Norris
<banorris@uci.edu>
Mon, 1 Oct 2012 20:29:54 +0000
(13:29 -0700)
action.cc
patch
|
blob
|
history
model.cc
patch
|
blob
|
history
diff --git
a/action.cc
b/action.cc
index 54ecce7dd4192e81c5e587041d2df7af27031de8..c744c65f1b5b06223ea08618c3ea1d1700b6c500 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();
}
}
}
}
diff --git
a/model.cc
b/model.cc
index 9d2dbb61ef577c43421f6ab071fe5fc7c9323004..47c6cdb92d442f0b0f460e353e9d25c93cfb6dc7 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();
}
}
}
}