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:
32  num_states(0)
33  {
34  }
35 
36  statet add_state();
38 
40  {
41  return accept_states.find(s)!=accept_states.end();
42  }
43 
45  {
46  accept_states.insert(s);
47  }
48 
51 
52  void reverse(goto_programt::targett epsilon);
53  void trim();
54 
55  std::size_t count_transitions();
56 
57  void output(std::ostream &str) const;
58 
59  void clear()
60  {
61  transitions.clear();
62  accept_states.clear();
63  num_states=0;
64  }
65 
66  void swap(automatont &that)
67  {
68  transitions.swap(that.transitions);
69  accept_states.swap(that.accept_states);
72  }
73 
74  static const statet no_state;
75 
76 // protected:
77  typedef std::multimap<goto_programt::targett, statet> transitionst;
78  typedef std::pair<transitionst::iterator, transitionst::iterator>
80  typedef std::vector<transitionst> transition_tablet;
81 
83  unsigned num_states;
86 };
87 
89 {
90  public:
91  explicit trace_automatont(goto_programt &_goto_program):
92  goto_program(_goto_program)
93  {
95  init_nta();
96 
98  epsilon++; // TODO: This is illegal.
99  }
100 
101  void add_path(patht &path);
102 
103  void build();
104 
106  {
107  return dta.init_state;
108  }
109 
110  void accept_states(state_sett &states)
111  {
112  states.insert(dta.accept_states.begin(), dta.accept_states.end());
113  }
114 
115  typedef std::pair<statet, statet> state_pairt;
116  typedef std::multimap<goto_programt::targett, state_pairt> sym_mapt;
117  typedef std::pair<sym_mapt::iterator, sym_mapt::iterator> sym_range_pairt;
118 
119  void get_transitions(sym_mapt &transitions);
120 
121  unsigned num_states()
122  {
123  return dta.num_states;
124  }
125 
126  typedef std::set<goto_programt::targett> alphabett;
128 
129  protected:
130  void build_alphabet(goto_programt &program);
131  void init_nta();
132 
134  {
135  return alphabet.find(t)!=alphabet.end();
136  }
137 
139 
140  void determinise();
141  void epsilon_closure(state_sett &s);
142 
143  void minimise();
144  void reverse();
145 
149 
150  typedef std::map<state_sett, statet> state_mapt;
151 
154  std::vector<state_sett> unmarked_dstates;
156 
159 };
160 
161 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H
bool is_accepting(statet s)
unsigned num_states
std::vector< transitionst > transition_tablet
static const statet no_state
void set_accepting(statet s)
transition_tablet transitions
std::pair< transitionst::iterator, transitionst::iterator > transition_ranget
statet add_state()
void output(std::ostream &str) const
void move(statet s, goto_programt::targett a, state_sett &t)
void swap(automatont &that)
void reverse(goto_programt::targett epsilon)
statet init_state
void add_trans(statet s, goto_programt::targett a, statet t)
state_sett accept_states
std::size_t count_transitions()
std::multimap< goto_programt::targett, statet > transitionst
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
instructionst::iterator targett
Definition: goto_program.h:550
bool in_alphabet(goto_programt::targett t)
goto_programt::targett epsilon
void get_transitions(sym_mapt &transitions)
statet find_dstate(state_sett &s)
void add_dtrans(state_sett &s, goto_programt::targett a, state_sett &t)
statet add_dstate(state_sett &s)
trace_automatont(goto_programt &_goto_program)
void accept_states(state_sett &states)
std::multimap< goto_programt::targett, state_pairt > sym_mapt
void build_alphabet(goto_programt &program)
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
std::vector< state_sett > unmarked_dstates
std::map< state_sett, statet > state_mapt
std::set< goto_programt::targett > alphabett
std::pair< statet, statet > state_pairt
unsigned num_states()
void add_path(patht &path)
void epsilon_closure(state_sett &s)
goto_programt & goto_program
void pop_unmarked_dstate(state_sett &s)
Concrete Goto Program.
Loop Acceleration.
std::list< path_nodet > patht
Definition: path.h:45
std::set< statet > state_sett
unsigned int statet