X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=model.cc;h=7808b104969f72fd9f9b62fe25a8574fffdac9b5;hp=2fa54d6e9ba1e76be577ec0625f6138ee7d1c5d4;hb=d884d14a6288f1ee1809158e81ffb05bf83f483b;hpb=35c057636dd12235368cfb9644532c7561609624;ds=inline diff --git a/model.cc b/model.cc index 2fa54d6..7808b10 100644 --- a/model.cc +++ b/model.cc @@ -388,7 +388,7 @@ void ModelChecker::set_backtracking(ModelAction *act) break; /* Don't backtrack into a point where the thread is disabled or sleeping. */ - if (node->get_enabled_array()[i]!=THREAD_ENABLED) + if (node->enabled_status(tid)!=THREAD_ENABLED) continue; /* Check if this has been explored already */ @@ -2025,7 +2025,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) { while(true) { Node *prevnode=write->get_node()->get_parent(); - bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET; + + bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET; if (write->is_release()&&thread_sleep) return true; if (!write->is_rmw()) {