cprover
|
#include <trace_automaton.h>
Public Types | |
typedef std::multimap< goto_programt::targett, statet > | transitionst |
typedef std::pair< transitionst::iterator, transitionst::iterator > | transition_ranget |
typedef std::vector< transitionst > | transition_tablet |
Public Member Functions | |
automatont () | |
statet | add_state () |
void | add_trans (statet s, goto_programt::targett a, statet t) |
bool | is_accepting (statet s) |
void | set_accepting (statet s) |
void | move (statet s, goto_programt::targett a, state_sett &t) |
void | move (state_sett &s, goto_programt::targett a, state_sett &t) |
void | reverse (goto_programt::targett epsilon) |
void | trim () |
std::size_t | count_transitions () |
void | output (std::ostream &str) |
void | clear () |
void | swap (automatont &that) |
Public Attributes | |
statet | init_state |
statet | accept_state |
statet | num_states |
transition_tablet | transitions |
state_sett | accept_states |
Definition at line 27 of file trace_automaton.h.
typedef std::pair<transitionst::iterator, transitionst::iterator> automatont::transition_ranget |
Definition at line 75 of file trace_automaton.h.
typedef std::vector<transitionst> automatont::transition_tablet |
Definition at line 76 of file trace_automaton.h.
typedef std::multimap<goto_programt::targett, statet> automatont::transitionst |
Definition at line 73 of file trace_automaton.h.
|
inline |
Definition at line 30 of file trace_automaton.h.
statet automatont::add_state | ( | ) |
Definition at line 277 of file trace_automaton.cpp.
References num_states, and transitions.
Referenced by trace_automatont::add_dstate(), trace_automatont::add_path(), trace_automatont::init_nta(), and reverse().
void automatont::add_trans | ( | statet | s, |
goto_programt::targett | a, | ||
statet | t | ||
) |
Definition at line 288 of file trace_automaton.cpp.
References transitions.
Referenced by trace_automatont::add_dtrans(), trace_automatont::add_path(), trace_automatont::init_nta(), and reverse().
|
inline |
Definition at line 57 of file trace_automaton.h.
References accept_states, num_states, and transitions.
Referenced by trace_automatont::determinise().
std::size_t automatont::count_transitions | ( | ) |
Definition at line 491 of file trace_automaton.cpp.
References transitions.
Referenced by trace_automatont::determinise().
|
inline |
Definition at line 37 of file trace_automaton.h.
References accept_states.
Referenced by trace_automatont::add_dstate().
void automatont::move | ( | statet | s, |
goto_programt::targett | a, | ||
state_sett & | t | ||
) |
Definition at line 313 of file trace_automaton.cpp.
References transitions.
Referenced by trace_automatont::determinise(), trace_automatont::epsilon_closure(), and move().
void automatont::move | ( | state_sett & | s, |
goto_programt::targett | a, | ||
state_sett & | t | ||
) |
Definition at line 329 of file trace_automaton.cpp.
References move().
void automatont::output | ( | std::ostream & | str | ) |
Definition at line 468 of file trace_automaton.cpp.
References accept_states, init_state, and transitions.
Referenced by trace_automatont::build().
void automatont::reverse | ( | goto_programt::targett | epsilon | ) |
Definition at line 358 of file trace_automaton.cpp.
References accept_states, add_state(), add_trans(), init_state, num_states, set_accepting(), and transitions.
Referenced by trace_automatont::minimise().
|
inline |
Definition at line 42 of file trace_automaton.h.
References accept_states.
Referenced by trace_automatont::add_dstate(), trace_automatont::add_path(), and reverse().
|
inline |
Definition at line 64 of file trace_automaton.h.
References accept_states, init_state, num_states, and transitions.
Referenced by trace_automatont::minimise().
void automatont::trim | ( | ) |
Definition at line 415 of file trace_automaton.cpp.
References accept_states, init_state, num_states, and transitions.
Referenced by trace_automatont::determinise().
statet automatont::accept_state |
Definition at line 79 of file trace_automaton.h.
state_sett automatont::accept_states |
Definition at line 82 of file trace_automaton.h.
Referenced by trace_automatont::accept_states(), clear(), trace_automatont::determinise(), is_accepting(), output(), reverse(), set_accepting(), swap(), and trim().
statet automatont::init_state |
Definition at line 78 of file trace_automaton.h.
Referenced by trace_automatont::add_path(), trace_automatont::determinise(), trace_automatont::init_nta(), trace_automatont::init_state(), output(), reverse(), swap(), and trim().
statet automatont::num_states |
Definition at line 80 of file trace_automaton.h.
Referenced by add_state(), clear(), trace_automatont::determinise(), trace_automatont::num_states(), reverse(), swap(), and trim().
transition_tablet automatont::transitions |
Definition at line 81 of file trace_automaton.h.
Referenced by add_state(), add_trans(), clear(), count_transitions(), trace_automatont::get_transitions(), move(), output(), reverse(), swap(), and trim().