spot::couvreur99_check_status Class Reference

The status of the emptiness-check on success. More...

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

Collaboration diagram for spot::couvreur99_check_status:

Public Member Functions
	couvreur99_check_status (const const_twa_ptr &aut)
	Construct a status object for the given automaton.
void	print_stats (std::ostream &os) const
	Output statistics about this object.
int	states () const
	Return the number of states visited by the search.

Public Attributes
const_twa_ptr	aut
	The automaton being checked.
scc_stack	root
	Stack of SCCs found during DFS.
state_map< int >	h
	Map from state to its DFS order number.
const state *	cycle_seed
	Seed state for the accepting cycle.

Detailed Description

The status of the emptiness-check on success.

This contains everything needed to construct a counter-example: the automaton, the stack of SCCs traversed by the counter-example, and the heap of visited states with their indexes.

Constructor & Destructor Documentation

couvreur99_check_status()

spot::couvreur99_check_status::couvreur99_check_status

(

const const_twa_ptr &

aut

)

Construct a status object for the given automaton.

Member Function Documentation

print_stats()

void spot::couvreur99_check_status::print_stats

(

std::ostream &

os

)

const

Output statistics about this object.

states()

int spot::couvreur99_check_status::states

(

)

const

Return the number of states visited by the search.

Member Data Documentation

aut

const_twa_ptr spot::couvreur99_check_status::aut

The automaton being checked.

cycle_seed

const state* spot::couvreur99_check_status::cycle_seed

Seed state for the accepting cycle.

h

state_map<int> spot::couvreur99_check_status::h

Map from state to its DFS order number.

root

scc_stack spot::couvreur99_check_status::root

Stack of SCCs found during DFS.

---

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

• spot/twaalgos/gtec/status.hh