spot::zielonka_tree Class Reference

Zielonka Tree implementation. More...

#include <spot/twaalgos/zlktree.hh>

Collaboration diagram for spot::zielonka_tree:

Classes
struct	zielonka_node

Public Member Functions
	zielonka_tree (const acc_cond &cond, zielonka_tree_options opt=zielonka_tree_options::NONE)
	Build a Zielonka tree from the acceptance condition. More...
unsigned	num_branches () const
	The number of branches in the Zielonka tree. More...
unsigned	first_branch () const
	The number of one branch in the tree. More...
std::pair< unsigned, unsigned >	step (unsigned branch, acc_cond::mark_t colors) const
	Walk through the Zielonka tree. More...
bool	is_even () const
	Whether the tree corresponds to a min even or min odd parity acceptance. More...
bool	has_rabin_shape () const
	Whether the Zielonka tree has Rabin shape. More...
bool	has_streett_shape () const
	Whether the Zielonka tree has Streett shape. More...
bool	has_parity_shape () const
	Whether the Zielonka tree has parity shape. More...
void	dot (std::ostream &) const
	Render the tree as in GraphViz format. More...

Public Attributes
std::vector< zielonka_node >	nodes_

Detailed Description

Zielonka Tree implementation.

This class implements a Zielonka Tree, using conventions similar to those in [8]

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

Constructor & Destructor Documentation

zielonka_tree()

spot::zielonka_tree::zielonka_tree	(	const acc_cond &	cond,
		zielonka_tree_options	opt = zielonka_tree_options::NONE
	)

Build a Zielonka tree from the acceptance condition.

Member Function Documentation

dot()

void spot::zielonka_tree::dot

(

std::ostream &

)

const

Render the tree as in GraphViz format.

first_branch()

unsigned spot::zielonka_tree::first_branch ( ) const

inline

The number of one branch in the tree.

This returns the branch whose leave is the smallest one.

has_parity_shape()

bool spot::zielonka_tree::has_parity_shape ( ) const

inline

Whether the Zielonka tree has parity shape.

The tree has parity shape of all nodes have at most one child.

has_rabin_shape()

bool spot::zielonka_tree::has_rabin_shape ( ) const

inline

Whether the Zielonka tree has Rabin shape.

The tree has Rabin shape of all accepting (round) nodes have at most one child.

has_streett_shape()

bool spot::zielonka_tree::has_streett_shape ( ) const

inline

Whether the Zielonka tree has Streett shape.

The tree has Streett shape of all rejecting (square) nodes have at most one child.

is_even()

bool spot::zielonka_tree::is_even ( ) const

inline

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

num_branches()

unsigned spot::zielonka_tree::num_branches ( ) const

inline

The number of branches in the Zielonka tree.

Branch are designated by the node number of their leaves.

step()

std::pair< unsigned, unsigned > spot::zielonka_tree::step	(	unsigned	branch,
		acc_cond::mark_t	colors
	)		const

Walk through the Zielonka tree.

Given a branch number, and a set of colors, this returns a pair (new branch, level), as needed in definition 3.3 of [8] (or definition 3.7 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().

This implementation is slightly different from the original definition since it allows a set of colors to be processed, and not exactly one color. When multiple colors are given, the minimum corresponding level is returned. When no color is given, the branch is not changed and the level returned might be one more than the depth of that branch (as if the tree had another layer of leaves labeled by the empty sets, that we do not store). Whether the depth for no color is the depth of the node or one more depend on whether the absence of color had the same parity has the current node.

---

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

• spot/twaalgos/zlktree.hh