cprover
Loading...
Searching...
No Matches
trace_automaton.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: 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
24typedef unsigned int statet;
25typedef std::set<statet> state_sett;
26
28{
29 public:
32 num_states(0)
33 {
34 }
35
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);
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
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();
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
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.
instructionst instructions
The list of instructions in the goto program.
instructionst::iterator targett
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
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:44
std::set< statet > state_sett
unsigned int statet