spot  2.11.6
Classes | Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
spot::twa_reachable_iterator_depth_first Class Reference

Iterate over all states of an automaton using a DFS. More...

#include <spot/twaalgos/reachiter.hh>

Inheritance diagram for spot::twa_reachable_iterator_depth_first:
Collaboration diagram for spot::twa_reachable_iterator_depth_first:

Classes

struct  stack_item
 

Public Member Functions

 twa_reachable_iterator_depth_first (const const_twa_ptr &a)
 
virtual void run ()
 Iterate over all reachable states of a spot::tgba. More...
 
virtual bool want_state (const state *s) const
 
virtual void start ()
 Called by run() before starting its iteration. More...
 
virtual void end ()
 Called by run() once all states have been explored. More...
 
virtual void process_state (const state *s, int n, twa_succ_iterator *si)
 
virtual void process_link (const state *in_s, int in, const state *out_s, int out, const twa_succ_iterator *si)
 

Protected Member Functions

virtual void push (const state *s, int sn)
 Push a new state in todo. More...
 
virtual void pop ()
 Pop the DFS stack. More...
 

Protected Attributes

const_twa_ptr aut_
 The spot::tgba to explore. More...
 
state_map< int > seen
 States already seen. More...
 
std::deque< stack_itemtodo
 the DFS stack More...
 

Detailed Description

Iterate over all states of an automaton using a DFS.

Member Function Documentation

◆ end()

virtual void spot::twa_reachable_iterator_depth_first::end ( )
virtual

Called by run() once all states have been explored.

◆ pop()

virtual void spot::twa_reachable_iterator_depth_first::pop ( )
protectedvirtual

Pop the DFS stack.

Reimplemented in spot::twa_reachable_iterator_depth_first_stack.

◆ process_link()

virtual void spot::twa_reachable_iterator_depth_first::process_link ( const state in_s,
int  in,
const state out_s,
int  out,
const twa_succ_iterator si 
)
virtual

Called by run() to process a transition.

Parameters
in_sThe source state
inThe source state number.
out_sThe destination state
outThe destination state number.
siThe spot::twa_succ_iterator positionned on the current transition.

The in_s and out_s states are owned by the spot::twa_reachable_iterator instance and destroyed when the instance is destroyed.

◆ process_state()

virtual void spot::twa_reachable_iterator_depth_first::process_state ( const state s,
int  n,
twa_succ_iterator si 
)
virtual

Called by run() to process a state.

Parameters
sThe current state.
nA unique number assigned to s.
siThe spot::twa_succ_iterator for s.

◆ push()

virtual void spot::twa_reachable_iterator_depth_first::push ( const state s,
int  sn 
)
protectedvirtual

Push a new state in todo.

Reimplemented in spot::twa_reachable_iterator_depth_first_stack.

◆ run()

virtual void spot::twa_reachable_iterator_depth_first::run ( )
virtual

Iterate over all reachable states of a spot::tgba.

This is a template method that will call start(), end(), want_state(), process_state(), and process_link(), while it iterates over states.

◆ start()

virtual void spot::twa_reachable_iterator_depth_first::start ( )
virtual

Called by run() before starting its iteration.

◆ want_state()

virtual bool spot::twa_reachable_iterator_depth_first::want_state ( const state s) const
virtual

Called by add_state or next_states implementations to filter states. Default implementation always return true.

Member Data Documentation

◆ aut_

const_twa_ptr spot::twa_reachable_iterator_depth_first::aut_
protected

The spot::tgba to explore.

◆ seen

state_map<int> spot::twa_reachable_iterator_depth_first::seen
protected

States already seen.

◆ todo

std::deque<stack_item> spot::twa_reachable_iterator_depth_first::todo
protected

the DFS stack


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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1