A version of spot::couvreur99_check that tries to visit known states first. More...

#include <spot/twaalgos/gtec/gtec.hh>

Inheritance diagram for spot::couvreur99_check_shy:

Collaboration diagram for spot::couvreur99_check_shy:

Classes
struct	successor
	A successor state with its associated acceptance marks, used in the shy Couvreur check. More...

struct	todo_item
	DFS stack item holding a state and its queue of unprocessed successors. More...

Public Types
typedef unsigned(unsigned_statistics::*	unsigned_fun) () const
	Function pointer type for unsigned statistics getters. More...

typedef std::map< const char *, unsigned_fun, char_ptr_less_than >	stats_map
	Map from statistic names to getter function pointers. More...

Public Member Functions
	couvreur99_check_shy (const const_twa_ptr &a, option_map o=option_map())
	Construct the shy variant for the given automaton and options. More...

virtual emptiness_check_result_ptr	check () override
	Check whether the automaton's language is empty. More...

virtual std::ostream &	print_stats (std::ostream &os) const override
	Print statistics, if any. More...

std::shared_ptr< const couvreur99_check_status >	result () const
	Return the status of the emptiness-check. More...

void	set_states (unsigned n)
	Set the number of visited states. More...

void	inc_states ()
	Increment the number of visited states. More...

void	inc_transitions ()
	Increment the number of visited transitions. More...

void	inc_depth (unsigned n=1)
	Increase the current DFS depth by n. More...

void	dec_depth (unsigned n=1)
	Decrease the current DFS depth by n. More...

unsigned	states () const
	Return the number of visited states. More...

unsigned	transitions () const
	Return the number of visited transitions. More...

unsigned	max_depth () const
	Return the maximum DFS depth reached. More...

unsigned	depth () const
	Return the current DFS depth. More...

unsigned	get (const char *str) const
	Retrieve a named statistic by its key. More...

const const_twa_ptr &	automaton () const
	The automaton that this emptiness-check inspects. More...

const option_map &	options () const
	Return the options parameterizing how the emptiness check is realized. More...

const char *	parse_options (char *options)
	Modify the algorithm options. More...

virtual bool	safe () const
	Return false iff accepting_run() can return 0 for non-empty automata. More...

virtual const unsigned_statistics *	statistics () const
	Return statistics, if available. More...

virtual const ec_statistics *	emptiness_check_statistics () const
	Return emptiness check statistics, if available. More...

virtual void	options_updated (const option_map &old)
	Notify option updates. More...

Public Attributes
stats_map	stats
	Map of available statistics. More...

Protected Types
typedef std::list< successor >	succ_queue
	Queue type for unprocessed successors of a state. More...

typedef std::list< todo_item >	todo_list
	List type for the DFS stack. More...

Protected Member Functions
void	clear_todo ()
	Clear the DFS stack. More...

void	remove_component (const state *start_delete)
	Remove a strongly component from the hash. More...

unsigned	get_removed_components () const
	Return the number of dead SCCs removed by the algorithm. More...

unsigned	get_vmsize () const
	Return the virtual memory size used by the process (in kB). More...

Protected Attributes
std::stack< acc_cond::mark_t >	arc
	Stack of inter-SCC acceptance marks. More...

int	num
	Counter of visited nodes (DFS order). More...

succ_queue::iterator	pos
	Iterator into current successor queue. More...

todo_list	todo
	The DFS stack. More...

bool	group_
	Whether successors should be grouped for states in the same SCC. More...

bool	group2_
	If set, reprocess successors of merged SCCs (implies group_). More...

std::shared_ptr< couvreur99_check_status >	ecs_
	Shared status object holding the DFS data structures. More...

bool	poprem_
	Whether to store the state to be removed. More...

unsigned	removed_components
	Number of dead SCC removed by the algorithm. More...

const_twa_ptr	a_
	The automaton. More...

option_map	o_
	The options. More...

Detailed Description

A version of spot::couvreur99_check that tries to visit known states first.

See the documentation for spot::couvreur99.

Member Typedef Documentation

◆ stats_map

typedef std::map<const char*, unsigned_fun, char_ptr_less_than> spot::unsigned_statistics::stats_map

inherited

Map from statistic names to getter function pointers.

◆ succ_queue

typedef std::list<successor> spot::couvreur99_check_shy::succ_queue

protected

Queue type for unprocessed successors of a state.

◆ todo_list

typedef std::list<todo_item> spot::couvreur99_check_shy::todo_list

protected

List type for the DFS stack.

◆ unsigned_fun

typedef unsigned(unsigned_statistics::* spot::unsigned_statistics::unsigned_fun) () const

inherited

Function pointer type for unsigned statistics getters.

Constructor & Destructor Documentation

◆ couvreur99_check_shy()

spot::couvreur99_check_shy::couvreur99_check_shy	(	const const_twa_ptr &	a,
		option_map	o = `option_map()`
	)

Construct the shy variant for the given automaton and options.

Member Function Documentation

◆ automaton()

const const_twa_ptr& spot::emptiness_check::automaton ( ) const

inlineinherited

The automaton that this emptiness-check inspects.

◆ check()

virtual emptiness_check_result_ptr spot::couvreur99_check_shy::check ( )

overridevirtual

Check whether the automaton's language is empty.

Reimplemented from spot::couvreur99_check.

◆ clear_todo()

void spot::couvreur99_check_shy::clear_todo ( )

protected

Clear the DFS stack.

◆ dec_depth()

void spot::ec_statistics::dec_depth ( unsigned n = 1 )

inlineinherited

Decrease the current DFS depth by n.

◆ depth()

unsigned spot::ec_statistics::depth ( ) const

inlineinherited

Return the current DFS depth.

◆ emptiness_check_statistics()

virtual const ec_statistics* spot::emptiness_check::emptiness_check_statistics ( ) const

virtualinherited

Return emptiness check statistics, if available.

◆ get()

unsigned spot::unsigned_statistics::get ( const char * str ) const

inlineinherited

Retrieve a named statistic by its key.

References spot::unsigned_statistics::stats.

◆ get_removed_components()

unsigned spot::couvreur99_check::get_removed_components ( ) const

protectedinherited

Return the number of dead SCCs removed by the algorithm.

◆ get_vmsize()

unsigned spot::couvreur99_check::get_vmsize ( ) const

protectedinherited

Return the virtual memory size used by the process (in kB).

◆ inc_depth()

void spot::ec_statistics::inc_depth ( unsigned n = 1 )

inlineinherited

Increase the current DFS depth by n.

◆ inc_states()

void spot::ec_statistics::inc_states ( )

inlineinherited

Increment the number of visited states.

◆ inc_transitions()

void spot::ec_statistics::inc_transitions ( )

inlineinherited

Increment the number of visited transitions.

◆ max_depth()

unsigned spot::ec_statistics::max_depth ( ) const

inlineinherited

Return the maximum DFS depth reached.

◆ options()

const option_map& spot::emptiness_check::options ( ) const

inlineinherited

Return the options parameterizing how the emptiness check is realized.

◆ options_updated()

virtual void spot::emptiness_check::options_updated ( const option_map & old )

virtualinherited

Notify option updates.

◆ parse_options()

const char* spot::emptiness_check::parse_options ( char * options )

inherited

Modify the algorithm options.

◆ print_stats()

virtual std::ostream& spot::couvreur99_check::print_stats ( std::ostream & os ) const

overridevirtualinherited

Print statistics, if any.

Reimplemented from spot::emptiness_check.

◆ remove_component()

void spot::couvreur99_check::remove_component ( const state * start_delete )

protectedinherited

Remove a strongly component from the hash.

This function remove all accessible state from a given state. In other words, it removes the strongly connected component that contains this state.

◆ result()

std::shared_ptr<const couvreur99_check_status> spot::couvreur99_check::result ( ) const

inherited

Return the status of the emptiness-check.

When check() succeed, the status should be passed along to spot::counter_example.

This status should not be deleted, it is a pointer to a member of this class that will be deleted when the couvreur99 object is deleted.

◆ safe()

virtual bool spot::emptiness_check::safe ( ) const

virtualinherited

Return false iff accepting_run() can return 0 for non-empty automata.

◆ set_states()

void spot::ec_statistics::set_states ( unsigned n )

inlineinherited

Set the number of visited states.

◆ states()

unsigned spot::ec_statistics::states ( ) const

inlineinherited

Return the number of visited states.

◆ statistics()

virtual const unsigned_statistics* spot::emptiness_check::statistics ( ) const

virtualinherited

Return statistics, if available.

◆ transitions()

unsigned spot::ec_statistics::transitions ( ) const

inlineinherited

Return the number of visited transitions.

Member Data Documentation

◆ a_

const_twa_ptr spot::emptiness_check::a_

protectedinherited

The automaton.

◆ arc

std::stack<acc_cond::mark_t> spot::couvreur99_check_shy::arc

protected

Stack of inter-SCC acceptance marks.

◆ ecs_

std::shared_ptr<couvreur99_check_status> spot::couvreur99_check::ecs_

protectedinherited

Shared status object holding the DFS data structures.

◆ group2_

bool spot::couvreur99_check_shy::group2_

protected

If set, reprocess successors of merged SCCs (implies group_).

◆ group_

bool spot::couvreur99_check_shy::group_

protected

Whether successors should be grouped for states in the same SCC.

◆ num

int spot::couvreur99_check_shy::num

protected

Counter of visited nodes (DFS order).

◆ o_

option_map spot::emptiness_check::o_

protectedinherited

The options.

◆ poprem_

bool spot::couvreur99_check::poprem_

protectedinherited

Whether to store the state to be removed.

◆ pos

succ_queue::iterator spot::couvreur99_check_shy::pos

protected

Iterator into current successor queue.

◆ removed_components

unsigned spot::couvreur99_check::removed_components

protectedinherited

Number of dead SCC removed by the algorithm.

◆ stats

stats_map spot::unsigned_statistics::stats

inherited

Map of available statistics.

Referenced by spot::unsigned_statistics::get().

◆ todo

todo_list spot::couvreur99_check_shy::todo

protected

The DFS stack.

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

spot/twaalgos/gtec/gtec.hh

Classes

Public Types

Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ stats_map

◆ succ_queue

◆ todo_list

◆ unsigned_fun

Constructor & Destructor Documentation

◆ couvreur99_check_shy()

Member Function Documentation

◆ automaton()

◆ check()

◆ clear_todo()

◆ dec_depth()

◆ depth()

◆ emptiness_check_statistics()

◆ get()

◆ get_removed_components()

◆ get_vmsize()

◆ inc_depth()

◆ inc_states()

◆ inc_transitions()

◆ max_depth()

◆ options()

◆ options_updated()

◆ parse_options()

◆ print_stats()

◆ remove_component()

◆ result()

◆ safe()

◆ set_states()

◆ states()

◆ statistics()

◆ transitions()

Member Data Documentation

◆ a_

◆ arc

◆ ecs_

◆ group2_

◆ group_

◆ num

◆ o_

◆ poprem_

◆ pos

◆ removed_components

◆ stats

◆ todo