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

Member Function Documentation

◆ accept_states()

void trace_automatont::accept_states ( state_sett states)
inline

Definition at line 107 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 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 alphabet.

Referenced by add_path().

◆ init_nta()

void trace_automatont::init_nta ( )
protected

◆ init_state()

int trace_automatont::init_state ( )
inline

Definition at line 102 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 458 of file trace_automaton.cpp.

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

◆ num_states()

int trace_automatont::num_states ( )
inline

Definition at line 118 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 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

◆ epsilon

goto_programt::targett trace_automatont::epsilon
protected

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

Referenced by trace_automatont().

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