cprover
trace_automatont Class Reference

#include <trace_automaton.h>

Collaboration diagram for trace_automatont:
[legend]

Public Types

typedef std::pair< statet, statetstate_pairt
 
typedef std::multimap< goto_programt::targett, state_pairtsym_mapt
 
typedef std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
 
typedef std::set< goto_programt::targettalphabett
 

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 88 of file trace_automaton.h.

Member Typedef Documentation

◆ alphabett

Definition at line 126 of file trace_automaton.h.

◆ state_mapt

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

Definition at line 150 of file trace_automaton.h.

◆ state_pairt

Definition at line 115 of file trace_automaton.h.

◆ sym_mapt

Definition at line 116 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 117 of file trace_automaton.h.

Constructor & Destructor Documentation

◆ trace_automatont()

trace_automatont::trace_automatont ( goto_programt _goto_program)
inlineexplicit

Member Function Documentation

◆ accept_states()

void trace_automatont::accept_states ( state_sett states)
inline

Definition at line 110 of file trace_automaton.h.

References automatont::accept_states, and dta.

Referenced by acceleratet::insert_automaton().

◆ add_dstate()

statet trace_automatont::add_dstate ( state_sett s)
protected

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

References automatont::add_trans(), CHECK_RETURN, dta, find_dstate(), and automatont::no_state.

Referenced by determinise().

◆ add_path()

void trace_automatont::add_path ( patht path)

◆ build()

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().

◆ build_alphabet()

void trace_automatont::build_alphabet ( goto_programt program)
protected

◆ determinise()

◆ epsilon_closure()

void trace_automatont::epsilon_closure ( state_sett s)
protected

Definition at line 190 of file trace_automaton.cpp.

References epsilon, automatont::move(), and nta.

Referenced by determinise().

◆ find_dstate()

statet trace_automatont::find_dstate ( state_sett s)
protected

Definition at line 268 of file trace_automaton.cpp.

References dstates, and automatont::no_state.

Referenced by add_dstate(), add_dtrans(), and determinise().

◆ get_transitions()

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().

◆ in_alphabet()

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

Definition at line 133 of file trace_automaton.h.

References alphabet.

Referenced by add_path().

◆ init_nta()

void trace_automatont::init_nta ( )
protected

◆ init_state()

statet trace_automatont::init_state ( )
inline

Definition at line 105 of file trace_automaton.h.

References dta, and automatont::init_state.

Referenced by acceleratet::insert_automaton().

◆ minimise()

void trace_automatont::minimise ( )
protected

Definition at line 466 of file trace_automaton.cpp.

References determinise(), dta, epsilon, nta, automatont::reverse(), and automatont::swap().

◆ num_states()

unsigned trace_automatont::num_states ( )
inline

Definition at line 121 of file trace_automaton.h.

References dta, and automatont::num_states.

Referenced by acceleratet::insert_automaton().

◆ pop_unmarked_dstate()

void trace_automatont::pop_unmarked_dstate ( state_sett s)
protected

Definition at line 181 of file trace_automaton.cpp.

References unmarked_dstates.

Referenced by determinise().

◆ reverse()

void trace_automatont::reverse ( )
protected

Member Data Documentation

◆ alphabet

alphabett trace_automatont::alphabet

◆ dstates

state_mapt trace_automatont::dstates
protected

Definition at line 155 of file trace_automaton.h.

Referenced by add_dstate(), determinise(), and find_dstate().

◆ dta

automatont trace_automatont::dta
protected

◆ epsilon

goto_programt::targett trace_automatont::epsilon
protected

Definition at line 153 of file trace_automaton.h.

Referenced by add_path(), determinise(), epsilon_closure(), minimise(), and trace_automatont().

◆ goto_program

goto_programt& trace_automatont::goto_program
protected

Definition at line 152 of file trace_automaton.h.

Referenced by trace_automatont().

◆ nta

automatont trace_automatont::nta
protected

◆ unmarked_dstates

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

Definition at line 154 of file trace_automaton.h.

Referenced by add_dstate(), determinise(), and pop_unmarked_dstate().


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