Algorithms for parity acceptance

Functions
bool	spot::is_colored (const const_twa_graph_ptr &aut)
	Return true iff aut is colored. More...
enum	spot::parity_kind { spot::parity_kind_max , spot::parity_kind_min , spot::parity_kind_same , spot::parity_kind_any }
	Parity kind type. More...
enum	spot::parity_style { spot::parity_style_odd , spot::parity_style_even , spot::parity_style_same , spot::parity_style_any }
	Parity style type. More...
twa_graph_ptr	spot::change_parity (const const_twa_graph_ptr &aut, parity_kind kind, parity_style style)
	Change the parity acceptance of an automaton. More...
twa_graph_ptr	spot::change_parity_here (twa_graph_ptr aut, parity_kind kind, parity_style style)
	Parity kind type. More...

Detailed Description

Enumeration Type Documentation

parity_kind

enum spot::parity_kind

#include <spot/twaalgos/parity.hh>

Parity kind type.

Enumerator
parity_kind_max	The new acceptance will be a parity max.
parity_kind_min	The new acceptance will be a parity min.
parity_kind_same	The new acceptance will keep the kind.
parity_kind_any	The new acceptance may change the kind.

parity_style

enum spot::parity_style

#include <spot/twaalgos/parity.hh>

Parity style type.

Enumerator
parity_style_odd	The new acceptance will be a parity odd.
parity_style_even	The new acceptance will be a parity even.
parity_style_same	The new acceptance will keep the style.
parity_style_any	The new acceptance may change the style.

Function Documentation

change_parity()

twa_graph_ptr spot::change_parity	(	const const_twa_graph_ptr &	aut,
		parity_kind	kind,
		parity_style	style
	)

#include <spot/twaalgos/parity.hh>

Change the parity acceptance of an automaton.

The parity acceptance condition of an automaton is characterized by

• The kind of the acceptance (min or max).
• The parity style, i.e., parity of the sets seen infinitely often (odd or even).
• The number of acceptance sets.

The output will be an equivalent automaton with the new parity acceptance. The number of acceptance sets may be increased by one. Every transition will belong to at most one acceptance set. The automaton must have a parity acceptance, otherwise an invalid_argument exception is thrown.

The parity kind is defined only if the number of acceptance sets is strictly greater than 1. The parity_style is defined only if the number of acceptance sets is non-zero. Some values of kind and style may result in equivalent outputs if the number of acceptance sets of the input automaton is not great enough.

Parameters

aut	the input automaton
kind	the parity kind of the output automaton
style	the parity style of the output automaton

Returns

the automaton with the new acceptance

change_parity_here()

twa_graph_ptr spot::change_parity_here	(	twa_graph_ptr	aut,
		parity_kind	kind,
		parity_style	style
	)

#include <spot/twaalgos/parity.hh>

Parity kind type.

is_colored()

bool spot::is_colored

(

const const_twa_graph_ptr &

aut

)

#include <spot/twaalgos/iscolored.hh>

Return true iff aut is colored.

An automaton is colored iff all the transitions belong to exactly one acceptance set. This function simply iterates over all the transitions.