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__element >	todo_
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:

• spot/mc/utils.hh