X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.h;h=a03ebca4bff1ca3a2fc950acbd33f043c49b2068;hb=4dd0204b6013e344a8728d27448cbf32f50825b6;hp=25401d9a3d349d07f6c4b11fe4a140e041f82394;hpb=0dc4895e7c40b9588d5ece94cba09e2fe2af420d;p=model-checker.git diff --git a/cyclegraph.h b/cyclegraph.h index 25401d9..a03ebca 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -9,19 +9,19 @@ #ifndef __CYCLEGRAPH_H__ #define __CYCLEGRAPH_H__ -#include #include #include #include "hashtable.h" #include "config.h" #include "mymemory.h" +#include "stl-model.h" class Promise; class CycleNode; class ModelAction; -typedef std::vector< const Promise *, ModelAlloc > promise_list_t; +typedef ModelVector promise_list_t; /** @brief A graph of Model Actions for tracking cycles. */ class CycleGraph { @@ -68,7 +68,7 @@ class CycleGraph { bool mergeNodes(CycleNode *node1, CycleNode *node2); HashTable *discovered; - std::vector< const CycleNode *, ModelAlloc > * queue; + ModelVector * queue; /** @brief A table for mapping ModelActions to CycleNodes */ @@ -77,7 +77,7 @@ class CycleGraph { HashTable promiseToNode; #if SUPPORT_MOD_ORDER_DUMP - std::vector< CycleNode *, SnapshotAlloc > nodeList; + SnapVector nodeList; #endif bool checkReachable(const CycleNode *from, const CycleNode *to) const; @@ -86,8 +86,8 @@ class CycleGraph { bool hasCycles; bool oldCycles; - std::vector< CycleNode *, SnapshotAlloc > rollbackvector; - std::vector< CycleNode *, SnapshotAlloc > rmwrollbackvector; + SnapVector rollbackvector; + SnapVector rmwrollbackvector; }; /** @@ -124,10 +124,10 @@ class CycleNode { const Promise *promise; /** @brief The edges leading out from this node */ - std::vector< CycleNode *, SnapshotAlloc > edges; + SnapVector edges; /** @brief The edges leading into this node */ - std::vector< CycleNode *, SnapshotAlloc > back_edges; + SnapVector back_edges; /** Pointer to a RMW node that reads from this node, or NULL, if none * exists */