X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=7241765d38c5270a33cf25a4986f5dd6fbd9a776;hb=85683f798e0955c43cf6cd8099713c45d9ce882b;hp=073b96b976cd4807c45c8c5e6ffef415941a0a81;hpb=7ba211ec7d1cacbaa3ef2027f1a0f534888f1708;p=model-checker.git diff --git a/model.h b/model.h index 073b96b..7241765 100644 --- a/model.h +++ b/model.h @@ -18,6 +18,7 @@ #include "clockvector.h" #include "hashtable.h" #include "workqueue.h" +#include "config.h" /* Forward declaration */ class NodeStack; @@ -25,7 +26,7 @@ class CycleGraph; class Promise; /** @brief Shorthand for a list of release sequence heads */ -typedef std::vector< const ModelAction *, MyAlloc > rel_heads_list_t; +typedef std::vector< const ModelAction *, ModelAlloc > rel_heads_list_t; /** * Model checker parameter structure. Holds run-time configuration options for @@ -66,6 +67,9 @@ public: /** Prints an execution summary with trace information. */ void print_summary(); +#if SUPPORT_MOD_ORDER_DUMP + void dumpGraph(char *filename); +#endif void add_thread(Thread *t); void remove_thread(Thread *t); @@ -74,7 +78,6 @@ public: thread_id_t get_next_id(); int get_num_threads(); - modelclock_t get_next_seq_num(); /** @return The currently executing Thread. */ Thread * get_current_thread() { return scheduler->get_current_thread(); } @@ -110,6 +113,8 @@ private: int num_feasible_executions; bool promises_expired(); + modelclock_t get_next_seq_num(); + /** * Stores the ModelAction for the current thread action. Call this * immediately before switching from user- to system-context to pass