cprover
Loading...
Searching...
No Matches
trace_automatont Class Reference

#include <trace_automaton.h>

Collaboration diagram for trace_automatont:

Public Types

typedef std::pair< statet, statetstate_pairt
typedef std::multimap< goto_programt::targett, state_pairt, goto_programt::target_less_thansym_mapt
typedef std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
typedef std::set< goto_programt::targett, goto_programt::target_less_thanalphabett

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, statetstate_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_programtgoto_program
goto_programt::targett epsilon
std::vector< state_settunmarked_dstates
state_mapt dstates
automatont nta
automatont dta

Detailed Description

Definition at line 90 of file trace_automaton.h.

Member Typedef Documentation

◆ alphabett

◆ state_mapt

typedef std::map<state_sett, statet> trace_automatont::state_mapt
protected

Definition at line 157 of file trace_automaton.h.

◆ state_pairt

Definition at line 117 of file trace_automaton.h.

◆ sym_mapt

◆ sym_range_pairt

typedef std::pair<sym_mapt::iterator, sym_mapt::iterator> trace_automatont::sym_range_pairt

Definition at line 123 of file trace_automaton.h.

Constructor & Destructor Documentation

◆ trace_automatont()

trace_automatont::trace_automatont ( goto_programt & _goto_program)
inlineexplicit

Definition at line 93 of file trace_automaton.h.

Member Function Documentation

◆ accept_states()

void trace_automatont::accept_states ( state_sett & states)
inline

Definition at line 112 of file trace_automaton.h.

◆ add_dstate()

statet trace_automatont::add_dstate ( state_sett & s)
protected

Definition at line 231 of file trace_automaton.cpp.

◆ add_dtrans()

void trace_automatont::add_dtrans ( state_sett & s,
goto_programt::targett a,
state_sett & t )
protected

Definition at line 307 of file trace_automaton.cpp.

◆ add_path()

void trace_automatont::add_path ( patht & path)

Definition at line 69 of file trace_automaton.cpp.

◆ build()

void trace_automatont::build ( )

Definition at line 24 of file trace_automaton.cpp.

◆ build_alphabet()

void trace_automatont::build_alphabet ( goto_programt & program)
protected

Definition at line 46 of file trace_automaton.cpp.

◆ determinise()

void trace_automatont::determinise ( )
protected

Definition at line 115 of file trace_automaton.cpp.

◆ epsilon_closure()

void trace_automatont::epsilon_closure ( state_sett & s)
protected

Definition at line 190 of file trace_automaton.cpp.

◆ find_dstate()

statet trace_automatont::find_dstate ( state_sett & s)
protected

Definition at line 268 of file trace_automaton.cpp.

◆ get_transitions()

void trace_automatont::get_transitions ( sym_mapt & transitions)

Definition at line 346 of file trace_automaton.cpp.

◆ in_alphabet()

bool trace_automatont::in_alphabet ( goto_programt::targett t)
inlineprotected

Definition at line 140 of file trace_automaton.h.

◆ init_nta()

void trace_automatont::init_nta ( )
protected

Definition at line 58 of file trace_automaton.cpp.

◆ init_state()

statet trace_automatont::init_state ( )
inline

Definition at line 107 of file trace_automaton.h.

◆ minimise()

void trace_automatont::minimise ( )
protected

Definition at line 466 of file trace_automaton.cpp.

◆ num_states()

unsigned trace_automatont::num_states ( )
inline

Definition at line 127 of file trace_automaton.h.

◆ pop_unmarked_dstate()

void trace_automatont::pop_unmarked_dstate ( state_sett & s)
protected

Definition at line 181 of file trace_automaton.cpp.

◆ reverse()

void trace_automatont::reverse ( )
protected

Member Data Documentation

◆ alphabet

alphabett trace_automatont::alphabet

Definition at line 134 of file trace_automaton.h.

◆ dstates

state_mapt trace_automatont::dstates
protected

Definition at line 162 of file trace_automaton.h.

◆ dta

automatont trace_automatont::dta
protected

Definition at line 165 of file trace_automaton.h.

◆ epsilon

goto_programt::targett trace_automatont::epsilon
protected

Definition at line 160 of file trace_automaton.h.

◆ goto_program

goto_programt& trace_automatont::goto_program
protected

Definition at line 159 of file trace_automaton.h.

◆ nta

automatont trace_automatont::nta
protected

Definition at line 164 of file trace_automaton.h.

◆ unmarked_dstates

std::vector<state_sett> trace_automatont::unmarked_dstates
protected

Definition at line 161 of file trace_automaton.h.


The documentation for this class was generated from the following files: