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.

Member Function Documentation

◆ add_state()

statet automatont::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.

References transitions.

Referenced by trace_automatont::determinise().

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

References move().

◆ output()

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

Definition at line 468 of file trace_automaton.cpp.

References accept_states, init_state, and transitions.

Referenced by trace_automatont::build().

◆ reverse()

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

◆ set_accepting()

void automatont::set_accepting ( statet  s)
inline

Definition at line 42 of file trace_automaton.h.

References accept_states.

Referenced by trace_automatont::add_dstate(), trace_automatont::add_path(), and reverse().

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

void automatont::trim ( )

Definition at line 415 of file trace_automaton.cpp.

References accept_states, init_state, num_states, and transitions.

Referenced by trace_automatont::determinise().

Member Data Documentation

◆ accept_state

statet automatont::accept_state

Definition at line 79 of file trace_automaton.h.

◆ accept_states

◆ init_state

◆ num_states

statet automatont::num_states

◆ transitions


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