X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=cyclegraph.h;h=81d736962dcb6893c8ef213b9571454c24ac5ea6;hb=f82a95581e303d67ea57de4ae9e888be10558866;hp=8a9bf7c928186ec3b39c0efd5022ae1ccfd8c1d1;hpb=a0562e0739fd643fdb2108f784f4722482ea5a4f;p=model-checker.git

diff --git a/cyclegraph.h b/cyclegraph.h
index 8a9bf7c..81d7369 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -9,6 +9,8 @@
 #include <vector>
 #include <inttypes.h>
 
+#include "mymemory.h"
+
 class CycleNode;
 class ModelAction;
 
@@ -19,6 +21,7 @@ class CycleGraph {
 	~CycleGraph();
 	void addEdge(const ModelAction *from, const ModelAction *to);
 	bool checkForCycles();
+	bool checkForRMWViolation();
 	void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
 
 	bool checkReachable(const ModelAction *from, const ModelAction *to);
@@ -26,6 +29,7 @@ class CycleGraph {
 	void commitChanges();
 	void rollbackChanges();
 
+	SNAPSHOTALLOC
  private:
 	CycleNode * getNode(const ModelAction *);
 
@@ -36,9 +40,11 @@ class CycleGraph {
 
 	/** @brief A flag: true if this graph contains cycles */
 	bool hasCycles;
-
 	bool oldCycles;
 
+	bool hasRMWViolation;
+	bool oldRMWViolation;
+
 	std::vector<CycleNode *> rollbackvector;
 	std::vector<CycleNode *> rmwrollbackvector;
 };
@@ -58,6 +64,7 @@ class CycleNode {
 		hasRMW=NULL;
 	}
 
+	SNAPSHOTALLOC
  private:
 	/** @brief The ModelAction that this node represents */
 	const ModelAction *action;