CBMC
Public Types | Public Member Functions | Public Attributes | Protected Types | Protected Member Functions | Protected Attributes | List of all members
trace_automatont Class Reference

#include <trace_automaton.h>

+ Collaboration diagram for trace_automatont:

Public Types

typedef std::pair< statet, statet > state_pairt
 
typedef std::multimap< goto_programt::targett, state_pairt, goto_programt::target_less_than > sym_mapt
 
typedef std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
 
typedef std::set< goto_programt::targett, goto_programt::target_less_than > 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
 

Detailed Description

Definition at line 90 of file trace_automaton.h.

Member Typedef Documentation

◆ alphabett

typedef std::set<goto_programt::targett, goto_programt::target_less_than> trace_automatont::alphabett

Definition at line 133 of file trace_automaton.h.

◆ state_mapt

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

Definition at line 157 of file trace_automaton.h.

◆ state_pairt

typedef std::pair<statet, statet> trace_automatont::state_pairt

Definition at line 117 of file trace_automaton.h.

◆ sym_mapt

typedef std::multimap< goto_programt::targett, state_pairt, goto_programt::target_less_than> trace_automatont::sym_mapt

Definition at line 122 of file trace_automaton.h.

◆ 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: