TωA representations

Modules
	MTDSwA (MTBDD-based ω-automata)
	Algorithms and data structures for MTBDD-based ω-automata.

Classes
class	spot::taa_tgba
	A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class, see below). More...
class	spot::set_state
class	spot::taa_succ_iterator
	Successor iterator for alternating automata with tree-and-automata (TAA) transitions. More...
class	spot::taa_tgba_string
	A TAA-TGBA automaton where states are labelled with strings. More...
class	spot::taa_tgba_formula
	A TAA-TGBA automaton where states are labelled with formulas. More...
struct	spot::twa_graph_state
	Graph-based representation of a TωA. More...
struct	spot::twa_graph_edge_data
	Data attached to edges of a twa_graph. More...
class	spot::twa_graph_succ_iterator< Graph >
	Iterator used by the on-the-fly interface of twa_graph. More...
class	spot::twa_graph
	Graph-based representation of a TωA. More...

Typedefs
typedef std::shared_ptr< const twa_graph >	spot::const_twa_graph_ptr
	Shared pointer to a const twa_graph. More...
typedef std::shared_ptr< twa_graph >	spot::twa_graph_ptr
	Shared pointer to a mutable twa_graph. More...
typedef std::shared_ptr< taa_tgba_string >	spot::taa_tgba_string_ptr
	Shared pointer to a taa_tgba_string automaton. More...
typedef std::shared_ptr< const taa_tgba_string >	spot::const_taa_tgba_string_ptr
	Shared pointer to a const taa_tgba_string automaton. More...
typedef std::shared_ptr< taa_tgba_formula >	spot::taa_tgba_formula_ptr
	Shared pointer to a taa_tgba_formula automaton. More...
typedef std::shared_ptr< const taa_tgba_formula >	spot::const_taa_tgba_formula_ptr
	Shared pointer to a const taa_tgba_formula automaton. More...

Functions
taa_tgba_string_ptr	spot::make_taa_tgba_string (const bdd_dict_ptr &dict)
	Construct a taa_tgba_string automaton. More...
taa_tgba_formula_ptr	spot::make_taa_tgba_formula (const bdd_dict_ptr &dict)
	Construct a taa_tgba_formula automaton. More...
twa_graph_ptr	spot::make_twa_graph (const bdd_dict_ptr &dict)
	Build an explicit automaton from all states of aut,. More...
twa_graph_ptr	spot::make_twa_graph (const twa_graph_ptr &aut, twa::prop_set p)
	Build an explicit automaton from all states of aut,. More...
twa_graph_ptr	spot::make_twa_graph (const const_twa_graph_ptr &aut, twa::prop_set p, bool preserve_name_properties=false)
	Clone a twa_graph. More...
twa_graph_ptr	spot::make_twa_graph (const const_twa_ptr &aut, twa::prop_set p, bool preserve_names=false, unsigned max_states=-(1U))
	Build an explicit automaton from all states of aut,. More...

Detailed Description

Typedef Documentation

const_taa_tgba_formula_ptr

typedef std::shared_ptr<const taa_tgba_formula> spot::const_taa_tgba_formula_ptr

#include <spot/twa/taatgba.hh>

Shared pointer to a const taa_tgba_formula automaton.

const_taa_tgba_string_ptr

typedef std::shared_ptr<const taa_tgba_string> spot::const_taa_tgba_string_ptr

#include <spot/twa/taatgba.hh>

Shared pointer to a const taa_tgba_string automaton.

const_twa_graph_ptr

typedef std::shared_ptr<const twa_graph> spot::const_twa_graph_ptr

#include <spot/twa/fwd.hh>

Shared pointer to a const twa_graph.

taa_tgba_formula_ptr

typedef std::shared_ptr<taa_tgba_formula> spot::taa_tgba_formula_ptr

#include <spot/twa/taatgba.hh>

Shared pointer to a taa_tgba_formula automaton.

taa_tgba_string_ptr

typedef std::shared_ptr<taa_tgba_string> spot::taa_tgba_string_ptr

#include <spot/twa/taatgba.hh>

Shared pointer to a taa_tgba_string automaton.

twa_graph_ptr

typedef std::shared_ptr<twa_graph> spot::twa_graph_ptr

#include <spot/twa/fwd.hh>

Shared pointer to a mutable twa_graph.

Function Documentation

make_taa_tgba_formula()

taa_tgba_formula_ptr spot::make_taa_tgba_formula ( const bdd_dict_ptr &  dict )

inline

#include <spot/twa/taatgba.hh>

Construct a taa_tgba_formula automaton.

make_taa_tgba_string()

taa_tgba_string_ptr spot::make_taa_tgba_string ( const bdd_dict_ptr &  dict )

inline

#include <spot/twa/taatgba.hh>

Construct a taa_tgba_string automaton.

make_twa_graph() [1/4]

twa_graph_ptr spot::make_twa_graph ( const bdd_dict_ptr &  dict )

inline

#include <spot/twa/twagraph.hh>

Build an explicit automaton from all states of aut,.

Referenced by spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::setup(), and spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::setup().

make_twa_graph() [2/4]

twa_graph_ptr spot::make_twa_graph ( const const_twa_graph_ptr &  aut, twa::prop_set  p, bool  preserve_name_properties = false  )

inline

#include <spot/twa/twagraph.hh>

Clone a twa_graph.

The p and preserve_name_properties argument are used to select what automata properties should be preserved by the copy.

make_twa_graph() [3/4]

twa_graph_ptr spot::make_twa_graph	(	const const_twa_ptr &	aut,
		twa::prop_set	p,
		bool	preserve_names = false,
		unsigned	max_states = -(1U)
	)

#include <spot/twa/twagraph.hh>

Build an explicit automaton from all states of aut,.

This overload works using the abstract interface for automata.

Set preserve_names to preserve state names, and set max_states to a maximum number of states to keep. States with successors that have not been kept will be marked as incomplete; this is mostly useful to display a subset of a large state space.

make_twa_graph() [4/4]

twa_graph_ptr spot::make_twa_graph ( const twa_graph_ptr &  aut, twa::prop_set  p  )

inline

#include <spot/twa/twagraph.hh>

Build an explicit automaton from all states of aut,.