projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
promise: rename has_sync_thread() -> thread_is_eliminated()
[model-checker.git]
/
promise.cc
diff --git
a/promise.cc
b/promise.cc
index 7b110020cd869514c0f958055fea357f9f3c42ba..3b2aa960f967bb389d48b24fe61e0d4f62664471 100644
(file)
--- a/
promise.cc
+++ b/
promise.cc
@@
-13,12
+13,12
@@
bool Promise::eliminate_thread(thread_id_t tid)
{
unsigned int id = id_to_int(tid);
bool Promise::eliminate_thread(thread_id_t tid)
{
unsigned int id = id_to_int(tid);
- if (id >=
sync
ed_thread.size())
-
sync
ed_thread.resize(id + 1, false);
- if (
sync
ed_thread[id])
+ if (id >=
eliminat
ed_thread.size())
+
eliminat
ed_thread.resize(id + 1, false);
+ if (
eliminat
ed_thread[id])
return false;
return false;
-
sync
ed_thread[id] = true;
+
eliminat
ed_thread[id] = true;
return has_failed();
}
return has_failed();
}
@@
-30,10
+30,10
@@
bool Promise::eliminate_thread(thread_id_t tid)
*/
bool Promise::has_failed() const
{
*/
bool Promise::has_failed() const
{
- unsigned int s
ync_size = sync
ed_thread.size();
+ unsigned int s
ize = eliminat
ed_thread.size();
int promise_tid = id_to_int(read->get_tid());
for (unsigned int i = 1; i < model->get_num_threads(); i++) {
int promise_tid = id_to_int(read->get_tid());
for (unsigned int i = 1; i < model->get_num_threads(); i++) {
- if ((i >= s
ync_size || !sync
ed_thread[i]) && ((int)i != promise_tid) && model->is_enabled(int_to_id(i))) {
+ if ((i >= s
ize || !eliminat
ed_thread[i]) && ((int)i != promise_tid) && model->is_enabled(int_to_id(i))) {
return false;
}
}
return false;
}
}