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
	DFS stack element pairing a state its with successor iterator. More...

Public Member Functions
	kripkecube_to_twa (kripkecube< State, SuccIterator > &sys, bdd_dict_ptr dict)
	Constructor for kripkecube-to-twa conversion.
	~kripkecube_to_twa ()
	Destructor.
void	run ()
	Run the conversion algorithm.
void	setup ()
	Setup algorithm resources.
bool	push (State s, unsigned i)
	Push state to stack.
bool	pop (State)
	Pop state from stack.
void	edge (unsigned src, unsigned dst)
	Add edge from src to dst.
void	finalize ()
	Finalize the result twa.
twa_graph_ptr	twa ()
	Return the resulting twa.

Protected Types
typedef std::unordered_map< const State, int, StateHash, StateEqual >	visited__map
	Type alias for visited map.

Protected Attributes
kripkecube< State, SuccIterator > &	sys_
	Reference to system model.
std::vector< todo__element >	todo_
	DFS todo stack.
visited__map	visited_
	Visited states map.
unsigned int	dfs_number_ = 0
	DFS numbering counter.
unsigned int	transitions_ = 0
	Transitions counter.
spot::twa_graph_ptr	res_
	Result twa.
std::vector< std::string > *	names_
	State names.
bdd_dict_ptr	dict_
	BDD dictionary.
std::unordered_map< int, int >	reverse_binder_
	Reverse binding for APs.

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.

Member Typedef Documentation

visited__map

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

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

protected

Type alias for visited map.

Constructor & Destructor Documentation

kripkecube_to_twa()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::kripkecube_to_twa ( kripkecube< State, SuccIterator > &  sys, bdd_dict_ptr  dict  )

inline

Constructor for kripkecube-to-twa conversion.

~kripkecube_to_twa()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::~kripkecube_to_twa ( )

inline

Destructor.

Member Function Documentation

edge()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

void spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::edge ( unsigned  src, unsigned  dst  )

inline

Add edge from src to dst.

References spot::cube_to_bdd().

finalize()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

void spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::finalize ( )

inline

Finalize the result twa.

pop()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

bool spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::pop ( State  )

inline

Pop state from stack.

push()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

bool spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::push ( State  s, unsigned  i  )

inline

Push state to stack.

run()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

void spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::run ( )

inline

Run the conversion algorithm.

setup()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

void spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::setup ( )

inline

Setup algorithm resources.

References spot::ap, spot::make_bdd_dict(), and spot::make_twa_graph().

twa()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

twa_graph_ptr spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::twa ( )

inline

Return the resulting twa.

Member Data Documentation

dfs_number_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

unsigned int spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::dfs_number_ = 0

protected

DFS numbering counter.

dict_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

bdd_dict_ptr spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::dict_

protected

BDD dictionary.

names_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

std::vector<std::string>* spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::names_

protected

State names.

res_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

spot::twa_graph_ptr spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::res_

protected

Result twa.

reverse_binder_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

std::unordered_map<int, int> spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::reverse_binder_

protected

Reverse binding for APs.

sys_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

kripkecube<State, SuccIterator>& spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::sys_

protected

Reference to system model.

todo_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

std::vector<todo__element> spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::todo_

protected

DFS todo stack.

transitions_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

unsigned int spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::transitions_ = 0

protected

Transitions counter.

visited_

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >

visited__map spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::visited_

protected

Visited states map.

---

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

• spot/mc/utils.hh