spot  2.11.6
Classes | Public Member Functions | Protected Types | Protected Attributes | List of all members
spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual > Class Template Reference

convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could. More...

#include <spot/mc/utils.hh>

Collaboration diagram for spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >:

Classes

struct  todo__element
 

Public Member Functions

 kripkecube_to_twa (kripkecube< State, SuccIterator > &sys, bdd_dict_ptr dict)
 
void run ()
 
void setup ()
 
bool push (State s, unsigned i)
 
bool pop (State)
 
void edge (unsigned src, unsigned dst)
 
void finalize ()
 
twa_graph_ptr twa ()
 

Protected Types

typedef std::unordered_map< const State, int, StateHash, StateEqual > visited__map
 

Protected Attributes

kripkecube< State, SuccIterator > & sys_
 
std::vector< todo__elementtodo_
 
visited__map visited_
 
unsigned int dfs_number_ = 0
 
unsigned int transitions_ = 0
 
spot::twa_graph_ptr res_
 
std::vector< std::string > * names_
 
bdd_dict_ptr dict_
 
std::unordered_map< int, int > reverse_binder_
 

Detailed Description

template<typename State, typename SuccIterator, typename StateHash, typename StateEqual>
class spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >

convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could.


The documentation for this class was generated from the following file:

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