X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=b3b517caed9c087b0ed1daaeb9a271c4a3a7bc20;hb=55f3acdb4bec3b2879e189a82d23e112aba79aed;hp=c0cc93eb0a80523eefc48f2fe7ec3c8119d8619c;hpb=4546308ab989c074f83d8607e16f13ffbcff494a;p=model-checker.git diff --git a/model.cc b/model.cc index c0cc93e..b3b517c 100644 --- a/model.cc +++ b/model.cc @@ -1,5 +1,6 @@ #include #include +#include #include "model.h" #include "action.h" @@ -11,7 +12,6 @@ #include "cyclegraph.h" #include "promise.h" #include "datarace.h" -#include "mutex.h" #include "threads-model.h" #define INITIAL_THREAD_ID 0 @@ -116,6 +116,10 @@ modelclock_t ModelChecker::get_next_seq_num() return ++priv->used_sequence_numbers; } +Node * ModelChecker::get_curr_node() { + return node_stack->get_head(); +} + /** * @brief Choose the next thread to execute. * @@ -767,10 +771,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(NULL); } - wake_up_sleeping_actions(curr); - ModelAction *newcurr = initialize_curr_action(curr); + wake_up_sleeping_actions(curr); /* Add the action to lists before any other model-checking tasks */ if (!second_part_of_rmw)