spot  2.8.1
Functions

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

#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

#include <spot/twaalgos/parity.hh>

Parity style type.

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
autthe input automaton
kindthe parity kind of the output automaton
stylethe 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.


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13