spot  2.11.6
Classes | Functions

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


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