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 () |
int | init_state () |
void | accept_states (state_sett &states) |
void | get_transitions (sym_mapt &transitions) |
int | 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 |
Static Protected Attributes | |
static const statet | no_state = -1 |
Definition at line 85 of file trace_automaton.h.
typedef std::set<goto_programt::targett> trace_automatont::alphabett |
Definition at line 123 of file trace_automaton.h.
|
protected |
Definition at line 148 of file trace_automaton.h.
typedef std::pair<statet, statet> trace_automatont::state_pairt |
Definition at line 112 of file trace_automaton.h.
typedef std::multimap<goto_programt::targett, state_pairt> trace_automatont::sym_mapt |
Definition at line 113 of file trace_automaton.h.
typedef std::pair<sym_mapt::iterator, sym_mapt::iterator> trace_automatont::sym_range_pairt |
Definition at line 114 of file trace_automaton.h.
|
inlineexplicit |
Definition at line 88 of file trace_automaton.h.
|
inline |
Definition at line 107 of file trace_automaton.h.
Referenced by acceleratet::insert_automaton(), automatont::output(), automatont::reverse(), and automatont::trim().
|
protected |
Definition at line 224 of file trace_automaton.cpp.
References automatont::add_state(), dstates, dta, find_dstate(), automatont::is_accepting(), no_state, nta, automatont::set_accepting(), and unmarked_dstates.
Referenced by determinise().
|
protected |
Definition at line 299 of file trace_automaton.cpp.
References automatont::add_trans(), dta, find_dstate(), and no_state.
Referenced by determinise().
void trace_automatont::add_path | ( | patht & | path | ) |
Definition at line 64 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 19 of file trace_automaton.cpp.
References determinise(), dta, nta, and automatont::output().
Referenced by acceleratet::restrict_traces().
|
protected |
Definition at line 41 of file trace_automaton.cpp.
References alphabet, Forall_goto_program_instructions, and goto_program_templatet< codeT, guardT >::get_successors().
|
protected |
Definition at line 110 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, automatont::move(), no_state, nta, automatont::num_states, pop_unmarked_dstate(), automatont::trim(), and unmarked_dstates.
Referenced by build(), and minimise().
|
protected |
Definition at line 183 of file trace_automaton.cpp.
References epsilon, automatont::move(), and nta.
Referenced by determinise().
|
protected |
Definition at line 260 of file trace_automaton.cpp.
References dstates, and no_state.
Referenced by add_dstate(), add_dtrans(), and determinise().
void trace_automatont::get_transitions | ( | sym_mapt & | transitions | ) |
Definition at line 338 of file trace_automaton.cpp.
References dta, and automatont::transitions.
Referenced by acceleratet::insert_automaton().
|
inlineprotected |
Definition at line 130 of file trace_automaton.h.
References automatont::reverse().
Referenced by add_path().
|
protected |
Definition at line 53 of file trace_automaton.cpp.
References automatont::add_state(), automatont::add_trans(), alphabet, automatont::init_state, and nta.
|
inline |
Definition at line 102 of file trace_automaton.h.
Referenced by acceleratet::insert_automaton(), automatont::output(), automatont::reverse(), and automatont::trim().
|
protected |
Definition at line 458 of file trace_automaton.cpp.
References determinise(), dta, epsilon, nta, automatont::reverse(), and automatont::swap().
|
inline |
Definition at line 118 of file trace_automaton.h.
Referenced by automatont::add_state(), acceleratet::insert_automaton(), automatont::reverse(), and automatont::trim().
|
protected |
Definition at line 174 of file trace_automaton.cpp.
References unmarked_dstates.
Referenced by determinise().
|
protected |
alphabett trace_automatont::alphabet |
Definition at line 124 of file trace_automaton.h.
Referenced by build_alphabet(), determinise(), init_nta(), and acceleratet::insert_automaton().
|
protected |
Definition at line 153 of file trace_automaton.h.
Referenced by add_dstate(), determinise(), and find_dstate().
|
protected |
Definition at line 156 of file trace_automaton.h.
Referenced by add_dstate(), add_dtrans(), build(), determinise(), get_transitions(), and minimise().
|
protected |
Definition at line 151 of file trace_automaton.h.
Referenced by add_path(), determinise(), epsilon_closure(), and minimise().
|
protected |
Definition at line 150 of file trace_automaton.h.
|
staticprotected |
Definition at line 143 of file trace_automaton.h.
Referenced by add_dstate(), add_dtrans(), determinise(), and find_dstate().
|
protected |
Definition at line 155 of file trace_automaton.h.
Referenced by add_dstate(), add_path(), build(), determinise(), epsilon_closure(), init_nta(), and minimise().
|
protected |
Definition at line 152 of file trace_automaton.h.
Referenced by add_dstate(), determinise(), and pop_unmarked_dstate().