spot::acd Class Reference

Alternating Cycle Decomposition implementation. More...

#include <spot/twaalgos/zlktree.hh>

Collaboration diagram for spot::acd:

Public Member Functions
	acd (const scc_info &si, acd_options opt=acd_options::NONE)
	Build a Alternating Cycle Decomposition an SCC decomposition. More...
	acd (const const_twa_graph_ptr &aut, acd_options opt=acd_options::NONE)
std::pair< unsigned, unsigned >	step (unsigned branch, unsigned edge) const
	Step through the ACD. More...
unsigned	state_step (unsigned node, unsigned edge) const
	Step through the ACD, with rules for state-based output. More...
std::vector< unsigned >	edges_of_node (unsigned n) const
	Return the list of edges covered by node n of the ACD. More...
unsigned	node_count () const
	Return the number of nodes in the the ACD forest. More...
bool	node_acceptance (unsigned n) const
unsigned	node_level (unsigned n) const
	Return the level of a node. More...
const acc_cond::mark_t &	node_colors (unsigned n) const
	Return the colors of a node. More...
bool	is_even (unsigned scc) const
	Whether the ACD corresponds to a min even or min odd parity acceptance in SCC scc. More...
bool	is_even () const
	Whether the ACD globally corresponds to a min even or min odd parity acceptance. More...
unsigned	first_branch (unsigned state) const
	Return the first branch for state. More...
unsigned	scc_max_level (unsigned scc) const
bool	has_rabin_shape () const
	Whether the ACD has Rabin shape. More...
bool	has_streett_shape () const
	Whether the ACD has Streett shape. More...
bool	has_parity_shape () const
	Whether the ACD has Streett shape. More...
const const_twa_graph_ptr	get_aut () const
	Return the automaton on which the ACD is defined. More...
void	dot (std::ostream &, const char *id=nullptr) const
	Render the ACD as in GraphViz format. More...

Detailed Description

Alternating Cycle Decomposition implementation.

This class implements an Alternating Cycle Decomposition similar to what is described in [8]

The differences is that this ACD is built from Emerson-Lei acceptance conditions, and can be "walked through" with multiple colors at once.

Constructor & Destructor Documentation

acd()

spot::acd::acd	(	const scc_info &	si,
		acd_options	opt = acd_options::NONE
	)

Build a Alternating Cycle Decomposition an SCC decomposition.

Member Function Documentation

dot()

void spot::acd::dot	(	std::ostream &	,
		const char *	id = nullptr
	)		const

Render the ACD as in GraphViz format.

If id is given, it is used to give the graph an id, and, all nodes will get ids as well.

edges_of_node()

std::vector<unsigned> spot::acd::edges_of_node

(

unsigned

n

)

const

Return the list of edges covered by node n of the ACD.

This is mostly used for interactive display.

first_branch()

unsigned spot::acd::first_branch

(

unsigned

state

)

const

Return the first branch for state.

get_aut()

const const_twa_graph_ptr spot::acd::get_aut ( ) const

inline

Return the automaton on which the ACD is defined.

has_parity_shape()

bool spot::acd::has_parity_shape

(

)

const

Whether the ACD has Streett shape.

The ACD has Streett shape if all nodes have no children with a state in common. The acd should be built with option CHECK_PARITY for this function to work.

has_rabin_shape()

bool spot::acd::has_rabin_shape

(

)

const

Whether the ACD has Rabin shape.

The ACD has Rabin shape if all accepting (round) nodes have no children with a state in common. The acd should be built with option CHECK_RABIN or CHECK_PARITY for this function to work.

has_streett_shape()

bool spot::acd::has_streett_shape

(

)

const

Whether the ACD has Streett shape.

The ACD has Streett shape if all rejecting (square) nodes have no children with a state in common. The acd should be built with option CHECK_STREETT or CHECK_PARITY for this function to work.

is_even() [1/2]

bool spot::acd::is_even ( ) const

inline

Whether the ACD globally corresponds to a min even or min odd parity acceptance.

The choice between even or odd is determined by the parity of the tallest tree of the ACD. In case two tree of opposite parity share the tallest height, then even parity is favored.

is_even() [2/2]

bool spot::acd::is_even ( unsigned  scc ) const

inline

Whether the ACD corresponds to a min even or min odd parity acceptance in SCC scc.

node_acceptance()

bool spot::acd::node_acceptance

(

unsigned

n

)

const

Tell whether a node store accepting or rejecting cycles.

This is mostly used for interactive display.

node_colors()

const acc_cond::mark_t& spot::acd::node_colors

(

unsigned

n

)

const

Return the colors of a node.

node_count()

unsigned spot::acd::node_count ( ) const

inline

Return the number of nodes in the the ACD forest.

node_level()

unsigned spot::acd::node_level

(

unsigned

n

)

const

Return the level of a node.

state_step()

unsigned spot::acd::state_step	(	unsigned	node,
		unsigned	edge
	)		const

Step through the ACD, with rules for state-based output.

Given a node number, and an edge, this returns the new node to associate to the destination state. This node is not necessarily a leave, and its level should be the level for the output state.

step()

std::pair<unsigned, unsigned> spot::acd::step	(	unsigned	branch,
		unsigned	edge
	)		const

Step through the ACD.

Given a branch number, and an edge, this returns a pair (new branch, level), as needed in definition 4.6 of [8] (or definition 4.20 in the full version).

The level correspond to the priority of a minimum parity acceptance condition, with the parity odd/even as specified by is_even().

---

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

• spot/twaalgos/zlktree.hh