spot::couvreur99_check Class Reference

An implementation of the Couvreur99 emptiness-check algorithm. More...

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

Inheritance diagram for spot::couvreur99_check:

Collaboration diagram for spot::couvreur99_check:

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 (const const_twa_ptr &a, option_map o=option_map())
	Construct an emptiness check 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 Member Functions
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::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

An implementation of the Couvreur99 emptiness-check algorithm.

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.

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

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

Construct an emptiness check 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::check ( )

overridevirtual

Check whether the automaton's language is empty.

Implements spot::emptiness_check.

Reimplemented in spot::couvreur99_check_shy.

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

protected

Return the number of dead SCCs removed by the algorithm.

get_vmsize()

unsigned spot::couvreur99_check::get_vmsize ( ) const

protected

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

overridevirtual

Print statistics, if any.

Reimplemented from spot::emptiness_check.

remove_component()

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

protected

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

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.

ecs_

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

protected

Shared status object holding the DFS data structures.

o_

option_map spot::emptiness_check::o_

protectedinherited

The options.

poprem_

bool spot::couvreur99_check::poprem_

protected

Whether to store the state to be removed.

removed_components

unsigned spot::couvreur99_check::removed_components

protected

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

---

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

• spot/twaalgos/gtec/gtec.hh