model: fixup style
[model-checker.git] / cyclegraph.h
1 /** @file cyclegraph.h @brief Data structure to track ordering
2  *  constraints on modification order.  The idea is to see whether a
3  *  total order exists that satisfies the ordering constriants.*/
4
5 #ifndef CYCLEGRAPH_H
6 #define CYCLEGRAPH_H
7
8 #include "hashtable.h"
9 #include <vector>
10 #include <inttypes.h>
11 #include "config.h"
12 #include "mymemory.h"
13
14 class CycleNode;
15 class ModelAction;
16
17 /** @brief A graph of Model Actions for tracking cycles. */
18 class CycleGraph {
19  public:
20         CycleGraph();
21         ~CycleGraph();
22         void addEdge(const ModelAction *from, const ModelAction *to);
23         bool checkForCycles();
24         bool checkForRMWViolation();
25         void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
26
27         bool checkReachable(const ModelAction *from, const ModelAction *to);
28         void startChanges();
29         void commitChanges();
30         void rollbackChanges();
31 #if SUPPORT_MOD_ORDER_DUMP
32         void dumpGraphToFile(const char * filename);
33 #endif
34
35         SNAPSHOTALLOC
36  private:
37         CycleNode * getNode(const ModelAction *);
38
39         /** @brief A table for mapping ModelActions to CycleNodes */
40         HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
41 #if SUPPORT_MOD_ORDER_DUMP
42         std::vector<CycleNode *> nodeList;
43 #endif
44
45         bool checkReachable(CycleNode *from, CycleNode *to);
46
47         /** @brief A flag: true if this graph contains cycles */
48         bool hasCycles;
49         bool oldCycles;
50
51         bool hasRMWViolation;
52         bool oldRMWViolation;
53
54         std::vector<CycleNode *> rollbackvector;
55         std::vector<CycleNode *> rmwrollbackvector;
56 };
57
58 /** @brief A node within a CycleGraph; corresponds to one ModelAction */
59 class CycleNode {
60  public:
61         CycleNode(const ModelAction *action);
62         bool addEdge(CycleNode * node);
63         std::vector<CycleNode *> * getEdges();
64         bool setRMW(CycleNode *);
65         CycleNode* getRMW();
66         const ModelAction * getAction() {return action;};
67
68         void popEdge() {
69                 edges.pop_back();
70         };
71         void clearRMW() {
72                 hasRMW=NULL;
73         }
74
75         SNAPSHOTALLOC
76  private:
77         /** @brief The ModelAction that this node represents */
78         const ModelAction *action;
79
80         /** @brief The edges leading out from this node */
81         std::vector<CycleNode *> edges;
82
83         /** Pointer to a RMW node that reads from this node, or NULL, if none
84          * exists */
85         CycleNode * hasRMW;
86 };
87
88 #endif