remove dead code... loop entrance condition is i<backtrack.size(). Therefore,
[model-checker.git] / cyclegraph.h
1 #ifndef CYCLEGRAPH_H
2 #define CYCLEGRAPH_H
3
4 #include "hashtable.h"
5 #include <vector>
6 #include <inttypes.h>
7
8 class CycleNode;
9 class ModelAction;
10
11 /** @brief A graph of Model Actions for tracking cycles. */
12 class CycleGraph {
13  public:
14         CycleGraph();
15         void addEdge(ModelAction *from, ModelAction *to);
16         bool checkForCycles();
17
18  private:
19         CycleNode * getNode(ModelAction *);
20         HashTable<ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
21         bool checkReachable(CycleNode *from, CycleNode *to);
22         bool hasCycles;
23
24 };
25
26 class CycleNode {
27  public:
28         CycleNode(ModelAction *action);
29         void addEdge(CycleNode * node);
30         std::vector<CycleNode *> * getEdges();
31
32  private:
33         ModelAction *action;
34         std::vector<CycleNode *> edges;
35 };
36
37 #endif