cprover
graph_visitor.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: graph visitor for computing edges involved for fencing
4 
5 Author: Vincent Nimal
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_MUSKETEER_GRAPH_VISITOR_H
13 #define CPROVER_MUSKETEER_GRAPH_VISITOR_H
14 
15 #include <set>
16 #include <list>
17 
19 
20 class fence_insertert;
21 
23 {
24 protected:
26 
28  std::set<event_idt> visited_nodes;
29 
30 public:
31  /* computes the PT (btwn), CT (cml) and IT (cntrl) */
32  void PT(const edget &e, std::set<unsigned> &edges);
33  void CT(const edget &e, std::set<unsigned> &edges);
34  void CT_not_powr(const edget &e, std::set<unsigned> &edges);
35  void IT(const edget &e, std::set<unsigned> &edges);
36 
38  event_grapht &graph,
39  event_idt next,
40  event_idt end,
41  std::list<event_idt> &old_path);
42  void graph_explore(event_grapht &graph, event_idt next, event_idt end,
43  std::list<event_idt> &old_path, std::set<unsigned> &edges);
44  void graph_explore_BC(event_grapht &egraph, event_idt next,
45  std::list<event_idt> &old_path, std::set<unsigned> &edges, bool porw);
46  void graph_explore_AC(event_grapht &egraph, event_idt next,
47  std::list<event_idt> &old_path, std::set<unsigned> &edges, bool porw);
49  event_grapht &egraph, event_idt next,
50  std::list<event_idt> &old_path,
51  std::set<unsigned> &edges)
52  {
53  graph_explore_BC(egraph, next, old_path, edges, false);
54  }
55 
57  event_grapht &egraph,
58  event_idt next,
59  std::list<event_idt> &old_path,
60  std::set<unsigned> &edges)
61  {
62  graph_explore_AC(egraph, next, old_path, edges, false);
63  }
64 
66  std::list<event_idt> &old_path);
68  std::list<event_idt> &old_path);
69 
70  explicit const_graph_visitort(fence_insertert &_fence_inserter)
71  : fence_inserter(_fence_inserter)
72  {}
73 };
74 
75 #endif // CPROVER_MUSKETEER_GRAPH_VISITOR_H
void graph_explore_BC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges)
Definition: graph_visitor.h:48
graph of abstract events
const_graph_visitort(fence_insertert &_fence_inserter)
Definition: graph_visitor.h:70
void CT_not_powr(const edget &e, std::set< unsigned > &edges)
void graph_explore_AC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges)
Definition: graph_visitor.h:56
void CT(const edget &e, std::set< unsigned > &edges)
event_grapht::critical_cyclet::delayt edget
Definition: graph_visitor.h:25
fence_insertert & fence_inserter
Definition: graph_visitor.h:27
wmm_grapht::node_indext event_idt
Definition: event_graph.h:32
void graph_explore(event_grapht &graph, event_idt next, event_idt end, std::list< event_idt > &old_path, std::set< unsigned > &edges)
void const_graph_explore(event_grapht &graph, event_idt next, event_idt end, std::list< event_idt > &old_path)
void graph_explore_BC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges, bool porw)
void graph_explore_AC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path, std::set< unsigned > &edges, bool porw)
void const_graph_explore_BC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path)
void const_graph_explore_AC(event_grapht &egraph, event_idt next, std::list< event_idt > &old_path)
void PT(const edget &e, std::set< unsigned > &edges)
std::set< event_idt > visited_nodes
Definition: graph_visitor.h:28
void IT(const edget &e, std::set< unsigned > &edges)