cprover
|
#include <trace_automaton.h>
Public Types | |
typedef std::pair< statet, statet > | state_pairt |
typedef std::multimap< goto_programt::targett, state_pairt > | sym_mapt |
typedef std::pair< sym_mapt::iterator, sym_mapt::iterator > | sym_range_pairt |
typedef std::set< goto_programt::targett > | alphabett |
Public Member Functions | |
trace_automatont (goto_programt &_goto_program) | |
void | add_path (patht &path) |
void | build () |
statet | init_state () |
void | accept_states (state_sett &states) |
void | get_transitions (sym_mapt &transitions) |
unsigned | num_states () |
Public Attributes | |
alphabett | alphabet |
Protected Types | |
typedef std::map< state_sett, statet > | state_mapt |
Protected Member Functions | |
void | build_alphabet (goto_programt &program) |
void | init_nta () |
bool | in_alphabet (goto_programt::targett t) |
void | pop_unmarked_dstate (state_sett &s) |
void | determinise () |
void | epsilon_closure (state_sett &s) |
void | minimise () |
void | reverse () |
statet | add_dstate (state_sett &s) |
statet | find_dstate (state_sett &s) |
void | add_dtrans (state_sett &s, goto_programt::targett a, state_sett &t) |
Protected Attributes | |
goto_programt & | goto_program |
goto_programt::targett | epsilon |
std::vector< state_sett > | unmarked_dstates |
state_mapt | dstates |
automatont | nta |
automatont | dta |
Definition at line 88 of file trace_automaton.h.
typedef std::set<goto_programt::targett> trace_automatont::alphabett |
Definition at line 126 of file trace_automaton.h.
|
protected |
Definition at line 150 of file trace_automaton.h.
typedef std::pair<statet, statet> trace_automatont::state_pairt |
Definition at line 115 of file trace_automaton.h.
typedef std::multimap<goto_programt::targett, state_pairt> trace_automatont::sym_mapt |
Definition at line 116 of file trace_automaton.h.
typedef std::pair<sym_mapt::iterator, sym_mapt::iterator> trace_automatont::sym_range_pairt |
Definition at line 117 of file trace_automaton.h.
|
inlineexplicit |
Definition at line 91 of file trace_automaton.h.
References build_alphabet(), epsilon, goto_program, init_nta(), and goto_programt::instructions.
|
inline |
Definition at line 110 of file trace_automaton.h.
References automatont::accept_states, and dta.
Referenced by acceleratet::insert_automaton().
|
protected |
Definition at line 231 of file trace_automaton.cpp.
References automatont::add_state(), dstates, dta, find_dstate(), INVARIANT, automatont::is_accepting(), automatont::no_state, nta, automatont::set_accepting(), and unmarked_dstates.
Referenced by determinise().
|
protected |
Definition at line 307 of file trace_automaton.cpp.
References automatont::add_trans(), CHECK_RETURN, dta, find_dstate(), and automatont::no_state.
Referenced by determinise().
void trace_automatont::add_path | ( | patht & | path | ) |
Definition at line 69 of file trace_automaton.cpp.
References automatont::add_state(), automatont::add_trans(), epsilon, in_alphabet(), automatont::init_state, nta, and automatont::set_accepting().
Referenced by acceleratet::restrict_traces().
void trace_automatont::build | ( | ) |
Definition at line 24 of file trace_automaton.cpp.
References determinise(), dta, nta, and automatont::output().
Referenced by acceleratet::restrict_traces().
|
protected |
Definition at line 46 of file trace_automaton.cpp.
References alphabet, Forall_goto_program_instructions, and goto_programt::get_successors().
Referenced by trace_automatont().
|
protected |
Definition at line 115 of file trace_automaton.cpp.
References automatont::accept_states, add_dstate(), add_dtrans(), alphabet, automatont::clear(), automatont::count_transitions(), dstates, dta, epsilon, epsilon_closure(), find_dstate(), automatont::init_state, INVARIANT, automatont::move(), automatont::no_state, nta, automatont::num_states, pop_unmarked_dstate(), automatont::trim(), and unmarked_dstates.
Referenced by build(), and minimise().
|
protected |
Definition at line 190 of file trace_automaton.cpp.
References epsilon, automatont::move(), and nta.
Referenced by determinise().
|
protected |
Definition at line 268 of file trace_automaton.cpp.
References dstates, and automatont::no_state.
Referenced by add_dstate(), add_dtrans(), and determinise().
void trace_automatont::get_transitions | ( | sym_mapt & | transitions | ) |
Definition at line 346 of file trace_automaton.cpp.
References dta, and automatont::transitions.
Referenced by acceleratet::insert_automaton().
|
inlineprotected |
|
protected |
Definition at line 58 of file trace_automaton.cpp.
References automatont::add_state(), automatont::add_trans(), alphabet, automatont::init_state, and nta.
Referenced by trace_automatont().
|
inline |
Definition at line 105 of file trace_automaton.h.
References dta, and automatont::init_state.
Referenced by acceleratet::insert_automaton().
|
protected |
Definition at line 466 of file trace_automaton.cpp.
References determinise(), dta, epsilon, nta, automatont::reverse(), and automatont::swap().
|
inline |
Definition at line 121 of file trace_automaton.h.
References dta, and automatont::num_states.
Referenced by acceleratet::insert_automaton().
|
protected |
Definition at line 181 of file trace_automaton.cpp.
References unmarked_dstates.
Referenced by determinise().
|
protected |
alphabett trace_automatont::alphabet |
Definition at line 127 of file trace_automaton.h.
Referenced by build_alphabet(), determinise(), in_alphabet(), init_nta(), and acceleratet::insert_automaton().
|
protected |
Definition at line 155 of file trace_automaton.h.
Referenced by add_dstate(), determinise(), and find_dstate().
|
protected |
Definition at line 158 of file trace_automaton.h.
Referenced by accept_states(), add_dstate(), add_dtrans(), build(), determinise(), get_transitions(), init_state(), minimise(), and num_states().
|
protected |
Definition at line 153 of file trace_automaton.h.
Referenced by add_path(), determinise(), epsilon_closure(), minimise(), and trace_automatont().
|
protected |
Definition at line 152 of file trace_automaton.h.
Referenced by trace_automatont().
|
protected |
Definition at line 157 of file trace_automaton.h.
Referenced by add_dstate(), add_path(), build(), determinise(), epsilon_closure(), init_nta(), and minimise().
|
protected |
Definition at line 154 of file trace_automaton.h.
Referenced by add_dstate(), determinise(), and pop_unmarked_dstate().