X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=0084fd3411cdb57e888b1dcef161eb16a6d1398d;hb=85d19a94bbe42390e82837ba75df5c39211a26f5;hp=bd98f5ca2f490f4c3743641ee7018d8e178d72ec;hpb=4fa31aac91303266f4c87a6cd5d60cbab34135db;p=model-checker.git diff --git a/action.cc b/action.cc index bd98f5c..0084fd3 100644 --- a/action.cc +++ b/action.cc @@ -1,6 +1,7 @@ #include #define __STDC_FORMAT_MACROS #include +#include #include "model.h" #include "action.h" @@ -499,9 +500,8 @@ void ModelAction::set_read_from_promise(Promise *promise) */ bool ModelAction::synchronize_with(const ModelAction *act) { - if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK) + if (*this < *act) return false; - model->check_promises(act->get_tid(), cv, act->cv); cv->merge(act->cv); return true; } @@ -618,7 +618,7 @@ void ModelAction::print() const if (reads_from) model_print(" Rf: %-3d", reads_from->get_seq_number()); else if (reads_from_promise) { - int idx = model->get_promise_number(reads_from_promise); + int idx = reads_from_promise->get_index(); if (idx >= 0) model_print(" Rf: P%-2d", idx); else @@ -648,7 +648,7 @@ unsigned int ModelAction::hash() const if (reads_from) hash ^= reads_from->get_seq_number(); else if (reads_from_promise) - hash ^= model->get_promise_number(reads_from_promise); + hash ^= reads_from_promise->get_index(); hash ^= get_reads_from_value(); } return hash;