X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=mutex.cc;h=d5ec40fff402df19093d68975c8a8914c0fa7567;hb=2d0d4ac38e05905a6633b3f2d5112ccadd45c27f;hp=0bb627d293b03a27d29673b3a95b1b3e136093c2;hpb=11bd7a3e906795b46b1fd20276a28002978bf1ab;p=model-checker.git diff --git a/mutex.cc b/mutex.cc index 0bb627d..d5ec40f 100644 --- a/mutex.cc +++ b/mutex.cc @@ -1,6 +1,7 @@ #include #include "model.h" +#include "execution.h" #include "threads-model.h" #include "clockvector.h" #include "action.h" @@ -9,10 +10,10 @@ namespace std { mutex::mutex() { - state.islocked = false; + state.locked = NULL; thread_id_t tid = thread_current()->get_id(); state.alloc_tid = tid; - state.alloc_clock = model->get_cv(tid)->getClock(tid); + state.alloc_clock = model->get_execution()->get_cv(tid)->getClock(tid); } void mutex::lock()