spot  2.4.4
Modules | Functions
TωA (Transition-based ω-Automata)

Modules

 Kripke Structures
 
 Essential TωA types
 
 TωA representations
 
 TωA algorithms
 

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)
 Build an explicit automaton from all states of aut,. 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

Spot is centered around the spot::twa type. This type and its cousins are listed here. This is an abstract interface. Its implementations are either concrete representations, or on-the-fly algorithms. Other algorithms that work on spot::twa are listed separately.

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 twa_graph_ptr &  aut,
twa::prop_set  p 
)
inline

#include <spot/twa/twagraph.hh>

Build an explicit automaton from all states of aut,.

◆ make_twa_graph() [3/4]

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

#include <spot/twa/twagraph.hh>

Build an explicit automaton from all states of aut,.

References spot::make_twa_graph(), and spot::U.

◆ make_twa_graph() [4/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.

Referenced by spot::make_twa_graph().


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Dec 25 2017 14:51:14 for spot by doxygen 1.8.13