import header file from specification
[model-checker.git] / cyclegraph.cc
1 #include "cyclegraph.h"
2 #include "action.h"
3
4 /** Initializes a CycleGraph object. */
5 CycleGraph::CycleGraph() {
6         hasCycles=false;
7 }
8
9 CycleGraph::~CycleGraph() {
10 }
11
12 /** Returns the CycleNode for a given ModelAction. */
13 CycleNode * CycleGraph::getNode(const ModelAction * action) {
14         CycleNode *node=actionToNode.get(action);
15         if (node==NULL) {
16                 node=new CycleNode(action);
17                 actionToNode.put(action, node);
18         }
19         return node;
20 }
21
22 /** Adds an edge between two ModelActions. */
23 void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
24         CycleNode *fromnode=getNode(from);
25         CycleNode *tonode=getNode(to);
26         if (!hasCycles) {
27                 // Check for Cycles
28                 hasCycles=checkReachable(tonode, fromnode);
29         }
30         fromnode->addEdge(tonode);
31 }
32
33 void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
34         CycleNode *fromnode=getNode(from);
35         CycleNode *rmwnode=getNode(rmw);
36
37         /* Two RMW actions cannot read from the same write. */
38         if (fromnode->setRMW())
39                 hasCycles=true;
40
41         /* Transfer all outgoing edges from the from node to the rmw node */
42         /* This process cannot add a cycle because rmw should not have any
43                  incoming edges yet.*/
44         std::vector<CycleNode *> * edges=fromnode->getEdges();
45         for(unsigned int i=0;edges->size();i++) {
46                 CycleNode * tonode=(*edges)[i];
47                 rmwnode->addEdge(tonode);
48         }
49         if (!hasCycles) {
50                 hasCycles=checkReachable(rmwnode, fromnode);
51         }
52         fromnode->addEdge(rmwnode);
53 }
54
55
56 /** Checks whether the first CycleNode can reach the second one. */
57 bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
58         std::vector<CycleNode *> queue;
59         HashTable<CycleNode *, CycleNode *, uintptr_t, 4> discovered;
60
61         queue.push_back(from);
62         discovered.put(from, from);
63         while(!queue.empty()) {
64                 CycleNode * node=queue.back();
65                 queue.pop_back();
66                 if (node==to)
67                         return true;
68
69                 for(unsigned int i=0;i<node->getEdges()->size();i++) {
70                         CycleNode *next=(*node->getEdges())[i];
71                         if (!discovered.contains(next)) {
72                                 discovered.put(next,next);
73                                 queue.push_back(next);
74                         }
75                 }
76         }
77         return false;
78 }
79
80 /** Returns whether a CycleGraph contains cycles. */
81 bool CycleGraph::checkForCycles() {
82         return hasCycles;
83 }
84
85 /** Constructor for a CycleNode. */
86 CycleNode::CycleNode(const ModelAction *modelaction) {
87         action=modelaction;
88 }
89
90 /** Returns a vector of the edges from a CycleNode. */
91 std::vector<CycleNode *> * CycleNode::getEdges() {
92         return &edges;
93 }
94
95 /** Adds an edge to a CycleNode. */
96 void CycleNode::addEdge(CycleNode * node) {
97         edges.push_back(node);
98 }
99
100 bool CycleNode::setRMW() {
101         bool oldhasRMW=hasRMW;
102         hasRMW=true;
103         return oldhasRMW;
104 }