Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 7808b104969f72fd9f9b62fe25a8574fffdac9b5..09e6b9da3150ddc88de4cc4b8ce363725cc493f3 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -218,7 +218,8 @@ void ModelChecker::execute_sleep_set() {
        for(unsigned int i=0;i<get_num_threads();i++) {
                thread_id_t tid=int_to_id(i);
                Thread *thr=get_thread(tid);
-               if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
+               if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
+                                thr->get_pending() == NULL ) {
                        thr->set_state(THREAD_RUNNING);
                        scheduler->next_thread(thr);
                        Thread::swap(&system_context, thr);
@@ -971,7 +972,7 @@ bool ModelChecker::promises_expired() {
 /** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
-       return promises->size() == 0 && pending_rel_seqs->size() == 0;
+       return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
 }
 
 /** @return whether the current partial trace is feasible. */
@@ -1094,7 +1095,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
                                ModelAction *act=*rit;
                                bool foundvalue = false;
                                for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
-                                       if (act->get_node()->get_read_from_at(i)==write) {
+                                       if (act->get_node()->get_read_from_at(j)==write) {
                                                foundvalue = true;
                                                break;
                                        }