cprover
automatont Class Reference

#include <trace_automaton.h>

Collaboration diagram for automatont:
[legend]

Public Types

typedef std::multimap< goto_programt::targett, statettransitionst
 
typedef std::pair< transitionst::iterator, transitionst::iterator > transition_ranget
 
typedef std::vector< transitionsttransition_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)
 
void clear ()
 
void swap (automatont &that)
 

Public Attributes

statet init_state
 
statet accept_state
 
statet num_states
 
transition_tablet transitions
 
state_sett accept_states
 

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

§ transition_tablet

Definition at line 76 of file trace_automaton.h.

§ transitionst

Definition at line 73 of file trace_automaton.h.

Constructor & Destructor Documentation

§ automatont()

automatont::automatont ( )
inline

Definition at line 30 of file trace_automaton.h.

References add_state(), and add_trans().

Member Function Documentation

§ add_state()

§ add_trans()

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

§ clear()

void automatont::clear ( void  )
inline

Definition at line 57 of file trace_automaton.h.

References accept_states, num_states, and transitions.

Referenced by trace_automatont::determinise().

§ count_transitions()

std::size_t automatont::count_transitions ( )

Definition at line 491 of file trace_automaton.cpp.

Referenced by trace_automatont::determinise(), and set_accepting().

§ is_accepting()

bool automatont::is_accepting ( statet  s)
inline

Definition at line 37 of file trace_automaton.h.

References accept_states.

Referenced by trace_automatont::add_dstate().

§ move() [1/2]

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

§ move() [2/2]

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

Definition at line 329 of file trace_automaton.cpp.

§ output()

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

§ reverse()

§ set_accepting()

void automatont::set_accepting ( statet  s)
inline

§ swap()

void automatont::swap ( automatont that)
inline

Definition at line 64 of file trace_automaton.h.

References accept_states, init_state, num_states, and transitions.

Referenced by trace_automatont::minimise().

§ trim()

Member Data Documentation

§ accept_state

statet automatont::accept_state

Definition at line 79 of file trace_automaton.h.

§ accept_states

state_sett automatont::accept_states

§ init_state

statet automatont::init_state

§ num_states

statet automatont::num_states

Definition at line 80 of file trace_automaton.h.

Referenced by clear(), trace_automatont::determinise(), and swap().

§ transitions

transition_tablet automatont::transitions

Definition at line 81 of file trace_automaton.h.

Referenced by clear(), trace_automatont::get_transitions(), and swap().


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