projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model: remove public check_promises() interface
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index f0c844cdcb019057cf6c110ad64a9d1d74cf4a4a..afb72b0aae490bda4a0464bb04837b380d81f4ca 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-1446,11
+1446,12
@@
bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
*/
bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second)
{
*/
bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second)
{
- if (
!second->synchronize_with(first)
) {
+ if (
*second < *first
) {
set_bad_synchronization();
return false;
}
set_bad_synchronization();
return false;
}
- return true;
+ check_promises(first->get_tid(), second->get_cv(), first->get_cv());
+ return second->synchronize_with(first);
}
/**
}
/**