spot::twa_reachable_iterator_depth_first_stack 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_stack:

Collaboration diagram for spot::twa_reachable_iterator_depth_first_stack:

Public Member Functions
	twa_reachable_iterator_depth_first_stack (const const_twa_ptr &a)
bool	on_stack (int sn) const
	Whether state sn is on the DFS stack. More...
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) override
	Push a new state in todo. More...
virtual void	pop () override
	Pop the DFS stack. More...

Protected Attributes
std::unordered_set< int >	stack_
const_twa_ptr	aut_
	The spot::tgba to explore. More...
state_map< int >	seen
	States already seen. More...
std::deque< stack_item >	todo
	the DFS stack More...

Detailed Description

Iterate over all states of an automaton using a DFS.

This variant also maintains a set of states that are on the DFS stack. It can be checked using the on_stack() method.

Member Function Documentation

end()

virtual void spot::twa_reachable_iterator_depth_first::end ( )

virtualinherited

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

on_stack()

bool spot::twa_reachable_iterator_depth_first_stack::on_stack

(

int

sn

)

const

Whether state sn is on the DFS stack.

Note the destination state of a transition is only pushed to the stack after process_link() has been called.

pop()

virtual void spot::twa_reachable_iterator_depth_first_stack::pop ( )

overrideprotectedvirtual

Pop the DFS stack.

Reimplemented from spot::twa_reachable_iterator_depth_first.

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  )

virtualinherited

Called by run() to process a transition.

Parameters

in_s	The source state
in	The source state number.
out_s	The destination state
out	The destination state number.
si	The 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  )

virtualinherited

Called by run() to process a state.

Parameters

s	The current state.
n	A unique number assigned to s.
si	The spot::twa_succ_iterator for s.

push()

virtual void spot::twa_reachable_iterator_depth_first_stack::push ( const state *  s, int  sn  )

overrideprotectedvirtual

Push a new state in todo.

Reimplemented from spot::twa_reachable_iterator_depth_first.

run()

virtual void spot::twa_reachable_iterator_depth_first::run ( )

virtualinherited

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

virtualinherited

Called by run() before starting its iteration.

want_state()

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

virtualinherited

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_

protectedinherited

The spot::tgba to explore.

seen

state_map<int> spot::twa_reachable_iterator_depth_first::seen

protectedinherited

States already seen.

todo

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

protectedinherited

the DFS stack

---

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

• spot/twaalgos/reachiter.hh