convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could.
More...
#include <spot/mc/utils.hh>
|
|
| 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 () |
| |
|
|
typedef std::unordered_map< const State, int, StateHash, StateEqual > | visited__map |
| |
|
|
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_ |
| |
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: