X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.h;h=a03ebca4bff1ca3a2fc950acbd33f043c49b2068;hb=d775a7d6624fa14284c4a273d039bedd21a1f55c;hp=d5c6a92af78715de0ff4f2c323a578b7a43f6ff1;hpb=7524803854c2de38c0311fe5037e3c17105ccfaa;p=model-checker.git diff --git a/cyclegraph.h b/cyclegraph.h index d5c6a92..a03ebca 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -9,19 +9,19 @@ #ifndef __CYCLEGRAPH_H__ #define __CYCLEGRAPH_H__ -#include "stl_wrappers.h" #include #include #include "hashtable.h" #include "config.h" #include "mymemory.h" +#include "stl-model.h" class Promise; class CycleNode; class ModelAction; -typedef model_vector< const Promise * > 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; - model_vector< const CycleNode * > * 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 */