cprover
trace_automaton.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H
14 
15 #include "path.h"
16 
18 
19 #include <map>
20 #include <vector>
21 #include <set>
22 #include <iosfwd>
23 
24 typedef unsigned int statet;
25 typedef std::set<statet> state_sett;
26 
28 {
29  public:
31  {
32  }
33 
34  statet add_state();
36 
38  {
39  return accept_states.find(s)!=accept_states.end();
40  }
41 
43  {
44  accept_states.insert(s);
45  }
46 
49 
50  void reverse(goto_programt::targett epsilon);
51  void trim();
52 
53  std::size_t count_transitions();
54 
55  void output(std::ostream &str);
56 
57  void clear()
58  {
59  transitions.clear();
60  accept_states.clear();
61  num_states=0;
62  }
63 
64  void swap(automatont &that)
65  {
66  transitions.swap(that.transitions);
67  accept_states.swap(that.accept_states);
70  }
71 
72 // protected:
73  typedef std::multimap<goto_programt::targett, statet> transitionst;
74  typedef std::pair<transitionst::iterator, transitionst::iterator>
76  typedef std::vector<transitionst> transition_tablet;
77 
81  transition_tablet transitions;
83 };
84 
86 {
87  public:
88  explicit trace_automatont(goto_programt &_goto_program):
89  goto_program(_goto_program)
90  {
91  build_alphabet(goto_program);
92  init_nta();
93 
94  epsilon=goto_program.instructions.end();
95  epsilon++;
96  }
97 
98  void add_path(patht &path);
99 
100  void build();
101 
103  {
104  return dta.init_state;
105  }
106 
107  void accept_states(state_sett &states)
108  {
109  states.insert(dta.accept_states.begin(), dta.accept_states.end());
110  }
111 
112  typedef std::pair<statet, statet> state_pairt;
113  typedef std::multimap<goto_programt::targett, state_pairt> sym_mapt;
114  typedef std::pair<sym_mapt::iterator, sym_mapt::iterator> sym_range_pairt;
115 
116  void get_transitions(sym_mapt &transitions);
117 
119  {
120  return dta.num_states;
121  }
122 
123  typedef std::set<goto_programt::targett> alphabett;
124  alphabett alphabet;
125 
126  protected:
127  void build_alphabet(goto_programt &program);
128  void init_nta();
129 
131  {
132  return alphabet.find(t)!=alphabet.end();
133  }
134 
135  void pop_unmarked_dstate(state_sett &s);
136 
137  void determinise();
138  void epsilon_closure(state_sett &s);
139 
140  void minimise();
141  void reverse();
142 
143  static const statet no_state = -1;
144  statet add_dstate(state_sett &s);
145  statet find_dstate(state_sett &s);
146  void add_dtrans(state_sett &s, goto_programt::targett a, state_sett &t);
147 
148  typedef std::map<state_sett, statet> state_mapt;
149 
152  std::vector<state_sett> unmarked_dstates;
153  state_mapt dstates;
154 
157 };
158 
159 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H
statet accept_state
std::pair< transitionst::iterator, transitionst::iterator > transition_ranget
std::multimap< goto_programt::targett, statet > transitionst
statet num_states
bool in_alphabet(goto_programt::targett t)
std::vector< transitionst > transition_tablet
void swap(automatont &that)
void accept_states(state_sett &states)
std::pair< statet, statet > state_pairt
void add_trans(statet s, goto_programt::targett a, statet t)
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
state_sett accept_states
bool is_accepting(statet s)
std::list< path_nodet > patht
Definition: path.h:45
std::size_t count_transitions()
std::set< statet > state_sett
statet add_state()
goto_programt & goto_program
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Loop Acceleration.
std::vector< state_sett > unmarked_dstates
std::multimap< goto_programt::targett, state_pairt > sym_mapt
std::set< goto_programt::targett > alphabett
std::map< state_sett, statet > state_mapt
trace_automatont(goto_programt &_goto_program)
void reverse(goto_programt::targett epsilon)
void move(statet s, goto_programt::targett a, state_sett &t)
transition_tablet transitions
goto_programt::targett epsilon
statet init_state
unsigned int statet
void output(std::ostream &str)
void set_accepting(statet s)
Concrete Goto Program.