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

Static Protected Attributes

static const statet no_state = -1
 

Detailed Description

Definition at line 85 of file trace_automaton.h.

Member Typedef Documentation

§ alphabett

Definition at line 123 of file trace_automaton.h.

§ state_mapt

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

Definition at line 148 of file trace_automaton.h.

§ state_pairt

Definition at line 112 of file trace_automaton.h.

§ sym_mapt

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

Constructor & Destructor Documentation

§ trace_automatont()

trace_automatont::trace_automatont ( goto_programt _goto_program)
inlineexplicit

Definition at line 88 of file trace_automaton.h.

Member Function Documentation

§ accept_states()

void trace_automatont::accept_states ( state_sett states)
inline

§ 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 299 of file trace_automaton.cpp.

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

Referenced by determinise().

§ add_path()

void trace_automatont::add_path ( patht path)

§ build()

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

§ 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 183 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 260 of file trace_automaton.cpp.

References dstates, and no_state.

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

§ get_transitions()

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

§ in_alphabet()

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

Definition at line 130 of file trace_automaton.h.

References automatont::reverse().

Referenced by add_path().

§ init_nta()

void trace_automatont::init_nta ( )
protected

§ init_state()

int trace_automatont::init_state ( )
inline

§ minimise()

void trace_automatont::minimise ( )
protected

Definition at line 458 of file trace_automaton.cpp.

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

§ num_states()

int trace_automatont::num_states ( )
inline

§ pop_unmarked_dstate()

void trace_automatont::pop_unmarked_dstate ( state_sett s)
protected

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

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

§ dta

automatont trace_automatont::dta
protected

Definition at line 156 of file trace_automaton.h.

Referenced by add_dstate(), add_dtrans(), build(), determinise(), get_transitions(), and minimise().

§ epsilon

goto_programt::targett trace_automatont::epsilon
protected

Definition at line 151 of file trace_automaton.h.

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

§ goto_program

goto_programt& trace_automatont::goto_program
protected

Definition at line 150 of file trace_automaton.h.

§ no_state

const statet trace_automatont::no_state = -1
staticprotected

Definition at line 143 of file trace_automaton.h.

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

§ nta

automatont trace_automatont::nta
protected

§ unmarked_dstates

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

Definition at line 152 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: