X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.h;h=d5c6a92af78715de0ff4f2c323a578b7a43f6ff1;hb=7524803854c2de38c0311fe5037e3c17105ccfaa;hp=a2cb93d7ca702217be5af879cbf0c2ba34f9a67e;hpb=e0f80c403452e544452f64687b3c489a869e4f77;p=model-checker.git diff --git a/cyclegraph.h b/cyclegraph.h index a2cb93d..d5c6a92 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -9,7 +9,7 @@ #ifndef __CYCLEGRAPH_H__ #define __CYCLEGRAPH_H__ -#include +#include "stl_wrappers.h" #include #include @@ -21,7 +21,7 @@ class Promise; class CycleNode; class ModelAction; -typedef std::vector< const Promise *, ModelAlloc > promise_list_t; +typedef model_vector< const Promise * > promise_list_t; /** @brief A graph of Model Actions for tracking cycles. */ class CycleGraph { @@ -53,8 +53,7 @@ class CycleGraph { void dot_print_edge(FILE *file, const T *from, const U *to, const char *prop); #endif - bool resolvePromise(const Promise *promise, ModelAction *writer, - promise_list_t *mustResolve); + bool resolvePromise(const Promise *promise, ModelAction *writer); SNAPSHOTALLOC private: @@ -66,10 +65,11 @@ class CycleGraph { CycleNode * getNode(const Promise *promise); CycleNode * getNode_noCreate(const ModelAction *act) const; CycleNode * getNode_noCreate(const Promise *promise) const; - bool mergeNodes(CycleNode *node1, CycleNode *node2, - promise_list_t *mustMerge); + bool mergeNodes(CycleNode *node1, CycleNode *node2); HashTable *discovered; + model_vector< const CycleNode * > * queue; + /** @brief A table for mapping ModelActions to CycleNodes */ HashTable actionToNode;