This class implements the sequential emptiness check as presented in "Three SCC-based Emptiness Checks for Generalized
Büchi Automata" (Renault et al, LPAR 2013). Among the three emptiness checks that have been proposed, we opted to implement yGabow's one.
More...
|
| | lpar13 (kripkecube< State, SuccIterator > &sys, twacube_ptr twa, shared_map &map, shared_struct *, unsigned tid, std::atomic< bool > &stop) |
| | Constructor for LPAR13 emptiness check.
|
| |
| virtual | ~lpar13 () |
| | Destructor.
|
| |
| bool | run () |
| | Run the algorithm.
|
| |
| void | setup () |
| | Setup thread resources.
|
| |
| bool | push_state (product_state, unsigned dfsnum, acc_cond::mark_t cond) |
| | Push product state to stack.
|
| |
| bool | pop_state (product_state, unsigned top_dfsnum, bool, product_state, unsigned) |
| | This method is called to notify the emptiness checks that a state will be popped. If the method returns false, then the state will be popped. Otherwise the state newtop will become the new top of the DFS stack. If the state top is the only one in the DFS stack, the parameter is_initial is set to true and both newtop and newtop_dfsnum have inconsistent values.
|
| |
| bool | update (product_state, unsigned, product_state, unsigned dst_dfsnum, acc_cond::mark_t cond) |
| | This method is called for every closing, back, or forward edge.
|
| |
| void | finalize () |
| | Finalize thread resources.
|
| |
| bool | finisher () |
| | Check if this thread finished the search.
|
| |
| unsigned int | states () |
| | Return number of states visited.
|
| |
| unsigned int | transitions () |
| | Return number of transitions traversed.
|
| |
| unsigned | walltime () |
| | Return wall time in milliseconds.
|
| |
| std::string | name () |
| | Return algorithm name.
|
| |
| int | sccs () |
| | Return number of SCCs found.
|
| |
| mc_rvalue | result () |
| | Return emptiness check result.
|
| |
| std::string | trace () |
| | Return trace.
|
| |
template<typename State, typename SuccIterator, typename StateHash, typename StateEqual>
class spot::lpar13< State, SuccIterator, StateHash, StateEqual >
This class implements the sequential emptiness check as presented in "Three SCC-based Emptiness Checks for Generalized
Büchi Automata" (Renault et al, LPAR 2013). Among the three emptiness checks that have been proposed, we opted to implement yGabow's one.
template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
| bool spot::lpar13< State, SuccIterator, StateHash, StateEqual >::pop_state |
( |
product_state |
, |
|
|
unsigned |
top_dfsnum, |
|
|
bool |
, |
|
|
product_state |
, |
|
|
unsigned |
|
|
) |
| |
|
inline |
This method is called to notify the emptiness checks that a state will be popped. If the method returns false, then the state will be popped. Otherwise the state newtop will become the new top of the DFS stack. If the state top is the only one in the DFS stack, the parameter is_initial is set to true and both newtop and newtop_dfsnum have inconsistent values.
template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
| bool spot::lpar13< State, SuccIterator, StateHash, StateEqual >::update |
( |
product_state |
, |
|
|
unsigned |
, |
|
|
product_state |
, |
|
|
unsigned |
dst_dfsnum, |
|
|
acc_cond::mark_t |
cond |
|
) |
| |
|
inline |
This method is called for every closing, back, or forward edge.
Return true if a counterexample has been found.
