spot::product_to_twa< State, SuccIterator, StateHash, StateEqual > Class Template Reference

Convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel. More...

#include <spot/mc/utils.hh>

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

Public Member Functions
	product_to_twa (kripkecube< State, SuccIterator > &sys, twacube_ptr twa)
	Constructor for product-to-twa conversion.
virtual	~product_to_twa ()
	Destructor.
bool	run ()
	Run the conversion algorithm.
twa_graph_ptr	twa ()
	Return the resulting twa.
void	setup ()
	Setup algorithm resources.
bool	push_state (product_state s, unsigned i, acc_cond::mark_t)
	Push product state to stack.
bool	update (product_state, unsigned src, product_state, unsigned dst, acc_cond::mark_t cond)
	Update state with acceptance condition.
bool	pop_state (product_state, unsigned, bool, product_state, unsigned)
	Pop state from stack.

Detailed Description

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

Convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel.

Constructor & Destructor Documentation

product_to_twa()

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

spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::product_to_twa ( kripkecube< State, SuccIterator > &  sys, twacube_ptr  twa  )

inline

Constructor for product-to-twa conversion.

~product_to_twa()

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

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

inlinevirtual

Destructor.

Member Function Documentation

pop_state()

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

bool spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::pop_state ( product_state  , unsigned  , bool  , product_state  , unsigned    )

inline

Pop state from stack.

push_state()

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

bool spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::push_state ( product_state  s, unsigned  i, acc_cond::mark_t    )

inline

Push product state to stack.

References spot::cube_to_bdd().

run()

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

bool spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::run ( )

inline

Run the conversion algorithm.

setup()

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

void spot::product_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::product_to_twa< State, SuccIterator, StateHash, StateEqual >::twa ( )

inline

Return the resulting twa.

update()

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

bool spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::update ( product_state  , unsigned  src, product_state  , unsigned  dst, acc_cond::mark_t  cond  )

inline

Update state with acceptance condition.

References spot::cube_to_bdd().

---

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

• spot/mc/utils.hh