X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=cyclegraph.h;h=c8e8956be10529d194304061f8f90a6c48181181;hp=81d736962dcb6893c8ef213b9571454c24ac5ea6;hb=e309adaee27786a638bcd44303ecb88351074257;hpb=04f478b27a93b7838f58a8480b9e3e22d41688f8 diff --git a/cyclegraph.h b/cyclegraph.h index 81d7369..c8e8956 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -8,7 +8,7 @@ #include "hashtable.h" #include #include - +#include "config.h" #include "mymemory.h" class CycleNode; @@ -28,6 +28,9 @@ class CycleGraph { void startChanges(); void commitChanges(); void rollbackChanges(); +#if SUPPORT_MOD_ORDER_DUMP + void dumpGraphToFile(const char * filename); +#endif SNAPSHOTALLOC private: @@ -35,6 +38,9 @@ class CycleGraph { /** @brief A table for mapping ModelActions to CycleNodes */ HashTable actionToNode; +#if SUPPORT_MOD_ORDER_DUMP + std::vector nodeList; +#endif bool checkReachable(CycleNode *from, CycleNode *to); @@ -53,10 +59,12 @@ class CycleGraph { class CycleNode { public: CycleNode(const ModelAction *action); - void addEdge(CycleNode * node); + bool addEdge(CycleNode * node); std::vector * getEdges(); bool setRMW(CycleNode *); CycleNode* getRMW(); + const ModelAction * getAction() {return action;}; + void popEdge() { edges.pop_back(); };