12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H 55 void output(std::ostream &str);
73 typedef std::multimap<goto_programt::targett, statet>
transitionst;
74 typedef std::pair<transitionst::iterator, transitionst::iterator>
89 goto_program(_goto_program)
91 build_alphabet(goto_program);
94 epsilon=goto_program.instructions.end();
98 void add_path(
patht &path);
104 return dta.init_state;
109 states.insert(dta.accept_states.begin(), dta.accept_states.end());
113 typedef std::multimap<goto_programt::targett, state_pairt>
sym_mapt;
120 return dta.num_states;
132 return alphabet.find(t)!=alphabet.end();
159 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H
std::pair< transitionst::iterator, transitionst::iterator > transition_ranget
std::multimap< goto_programt::targett, statet > transitionst
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
bool is_accepting(statet s)
std::list< path_nodet > patht
std::size_t count_transitions()
std::set< statet > state_sett
goto_programt & goto_program
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
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
void output(std::ostream &str)
void set_accepting(statet s)
instructionst::iterator targett