CBMC
Public Types | Public Member Functions | Public Attributes | Static Public Attributes | List of all members
automatont Class Reference

#include <trace_automaton.h>

+ Collaboration diagram for automatont:

Public Types

typedef std::multimap< goto_programt::targett, statet > transitionst
 
typedef std::pair< transitionst::iterator, transitionst::iterator > transition_ranget
 
typedef std::vector< transitionst > transition_tablet
 

Public Member Functions

 automatont ()
 
statet add_state ()
 
void add_trans (statet s, goto_programt::targett a, statet t)
 
bool is_accepting (statet s)
 
void set_accepting (statet s)
 
void move (statet s, goto_programt::targett a, state_sett &t)
 
void move (state_sett &s, goto_programt::targett a, state_sett &t)
 
void reverse (goto_programt::targett epsilon)
 
void trim ()
 
std::size_t count_transitions ()
 
void output (std::ostream &str) const
 
void clear ()
 
void swap (automatont &that)
 

Public Attributes

statet init_state
 
unsigned num_states
 
transition_tablet transitions
 
state_sett accept_states
 

Static Public Attributes

static const statet no_state =std::numeric_limits<statet>::max()
 

Detailed Description

Definition at line 27 of file trace_automaton.h.

Member Typedef Documentation

◆ transition_ranget

typedef std::pair<transitionst::iterator, transitionst::iterator> automatont::transition_ranget

Definition at line 79 of file trace_automaton.h.

◆ transition_tablet

typedef std::vector<transitionst> automatont::transition_tablet

Definition at line 80 of file trace_automaton.h.

◆ transitionst

typedef std::multimap<goto_programt::targett, statet> automatont::transitionst

Definition at line 77 of file trace_automaton.h.

Constructor & Destructor Documentation

◆ automatont()

automatont::automatont ( )
inline

Definition at line 30 of file trace_automaton.h.

Member Function Documentation

◆ add_state()

statet automatont::add_state ( )

Definition at line 285 of file trace_automaton.cpp.

◆ add_trans()

void automatont::add_trans ( statet  s,
goto_programt::targett  a,
statet  t 
)

Definition at line 296 of file trace_automaton.cpp.

◆ clear()

void automatont::clear ( )
inline

Definition at line 59 of file trace_automaton.h.

◆ count_transitions()

std::size_t automatont::count_transitions ( )

Definition at line 499 of file trace_automaton.cpp.

◆ is_accepting()

bool automatont::is_accepting ( statet  s)
inline

Definition at line 39 of file trace_automaton.h.

◆ move() [1/2]

void automatont::move ( state_sett &  s,
goto_programt::targett  a,
state_sett &  t 
)

Definition at line 337 of file trace_automaton.cpp.

◆ move() [2/2]

void automatont::move ( statet  s,
goto_programt::targett  a,
state_sett &  t 
)

Definition at line 321 of file trace_automaton.cpp.

◆ output()

void automatont::output ( std::ostream &  str) const

Definition at line 476 of file trace_automaton.cpp.

◆ reverse()

void automatont::reverse ( goto_programt::targett  epsilon)

Definition at line 366 of file trace_automaton.cpp.

◆ set_accepting()

void automatont::set_accepting ( statet  s)
inline

Definition at line 44 of file trace_automaton.h.

◆ swap()

void automatont::swap ( automatont &  that)
inline

Definition at line 66 of file trace_automaton.h.

◆ trim()

void automatont::trim ( )

Definition at line 423 of file trace_automaton.cpp.

Member Data Documentation

◆ accept_states

state_sett automatont::accept_states

Definition at line 85 of file trace_automaton.h.

◆ init_state

statet automatont::init_state

Definition at line 82 of file trace_automaton.h.

◆ no_state

const statet automatont::no_state =std::numeric_limits<statet>::max()
static

Definition at line 74 of file trace_automaton.h.

◆ num_states

unsigned automatont::num_states

Definition at line 83 of file trace_automaton.h.

◆ transitions

transition_tablet automatont::transitions

Definition at line 84 of file trace_automaton.h.

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