X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=41ec97b50bdb71744075d0216a4bb209813255a9;hb=bdef0741b8a01e16946d261bc2a657af5a683b3e;hp=b6099c69750b066d74d1d4a566834237edf3b097;hpb=1dbc6ce8102e79ead8c3ae09214126abab1b5c51;p=model-checker.git diff --git a/model.h b/model.h index b6099c6..41ec97b 100644 --- a/model.h +++ b/model.h @@ -16,10 +16,12 @@ #include "threads.h" #include "action.h" #include "clockvector.h" +#include "hashtable.h" /* Forward declaration */ class NodeStack; class CycleGraph; +class Promise; /** @brief The central structure for model-checking */ class ModelChecker { @@ -99,6 +101,7 @@ private: HashTable *obj_map; HashTable, uintptr_t, 4 > *obj_thrd_map; + std::vector * promises; std::vector *thrd_last_action; NodeStack *node_stack; ModelAction *next_backtrack;