X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=3dbd562755e41ece4f9836b9e6fa53a9c52c313f;hb=cf4cc8a444d3c85367b9aa15b91b2829220e2edf;hp=7241765d38c5270a33cf25a4986f5dd6fbd9a776;hpb=3b39a4cdcd7eafca5480e9d9bdec4d24fe5441b3;p=model-checker.git diff --git a/model.h b/model.h index 7241765..3dbd562 100644 --- a/model.h +++ b/model.h @@ -10,20 +10,19 @@ #include #include -#include "schedule.h" #include "mymemory.h" -#include "libthreads.h" -#include "threads.h" #include "action.h" -#include "clockvector.h" #include "hashtable.h" #include "workqueue.h" #include "config.h" +#include "modeltypes.h" /* Forward declaration */ class NodeStack; class CycleGraph; class Promise; +class Scheduler; +class Thread; /** @brief Shorthand for a list of release sequence heads */ typedef std::vector< const ModelAction *, ModelAlloc > rel_heads_list_t; @@ -73,14 +72,12 @@ public: void add_thread(Thread *t); void remove_thread(Thread *t); - Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); } - Thread * get_thread(ModelAction *act) { return get_thread(act->get_tid()); } + Thread * get_thread(thread_id_t tid) const; + Thread * get_thread(ModelAction *act) const; thread_id_t get_next_id(); int get_num_threads(); - - /** @return The currently executing Thread. */ - Thread * get_current_thread() { return scheduler->get_current_thread(); } + Thread * get_current_thread(); int switch_to_master(ModelAction *act); ClockVector * get_cv(thread_id_t tid);