TωA representations

Classes
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...

Functions
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

Function Documentation

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::copy().

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,.