spot  2.16
Classes | Public Types | Public Member Functions | Static Public Member Functions | List of all members
spot::lpar13< State, SuccIterator, StateHash, StateEqual > Class Template Reference
TωA (Transition-based ω-Automata) » Parallel Model Checking

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...

#include <spot/mc/lpar13.hh>

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

Public Types

using shared_map = int
 Type alias for shared map (useless for sequential algorithm) More...
 
using shared_struct = int
 Type alias for shared structure (useless here) More...
 

Public Member Functions

 lpar13 (kripkecube< State, SuccIterator > &sys, twacube_ptr twa, shared_map &map, shared_struct *, unsigned tid, std::atomic< bool > &stop)
 Constructor for LPAR13 emptiness check. More...
 
virtual ~lpar13 ()
 Destructor. More...
 
bool run ()
 Run the algorithm. More...
 
void setup ()
 Setup thread resources. More...
 
bool push_state (product_state, unsigned dfsnum, acc_cond::mark_t cond)
 Push product state to stack. More...
 
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. More...
 
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. More...
 
void finalize ()
 Finalize thread resources. More...
 
bool finisher ()
 Check if this thread finished the search. More...
 
unsigned int states ()
 Return number of states visited. More...
 
unsigned int transitions ()
 Return number of transitions traversed. More...
 
unsigned walltime ()
 Return wall time in milliseconds. More...
 
std::string name ()
 Return algorithm name. More...
 
int sccs ()
 Return number of SCCs found. More...
 
mc_rvalue result ()
 Return emptiness check result. More...
 
std::string trace ()
 Return trace. More...
 

Static Public Member Functions

static shared_struct * make_shared_structure (shared_map m, unsigned i)
 Create shared structure for thread tid. More...
 

Detailed Description

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.

Member Typedef Documentation

◆ shared_map

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
using spot::lpar13< State, SuccIterator, StateHash, StateEqual >::shared_map = int

Type alias for shared map (useless for sequential algorithm)

◆ shared_struct

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
using spot::lpar13< State, SuccIterator, StateHash, StateEqual >::shared_struct = int

Type alias for shared structure (useless here)

Constructor & Destructor Documentation

◆ lpar13()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
spot::lpar13< State, SuccIterator, StateHash, StateEqual >::lpar13 ( kripkecube< State, SuccIterator > &  sys,
twacube_ptr  twa,
shared_map &  map,
shared_struct *  ,
unsigned  tid,
std::atomic< bool > &  stop 
)
inline

Constructor for LPAR13 emptiness check.

References spot::U.

◆ ~lpar13()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
virtual spot::lpar13< State, SuccIterator, StateHash, StateEqual >::~lpar13 ( )
inlinevirtual

Destructor.

Member Function Documentation

◆ finalize()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
void spot::lpar13< State, SuccIterator, StateHash, StateEqual >::finalize ( )
inline

Finalize thread resources.

◆ finisher()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
bool spot::lpar13< State, SuccIterator, StateHash, StateEqual >::finisher ( )
inline

Check if this thread finished the search.

◆ make_shared_structure()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
static shared_struct* spot::lpar13< State, SuccIterator, StateHash, StateEqual >::make_shared_structure ( shared_map  m,
unsigned  i 
)
inlinestatic

Create shared structure for thread tid.

◆ name()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
std::string spot::lpar13< State, SuccIterator, StateHash, StateEqual >::name ( )
inline

Return algorithm name.

◆ pop_state()

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.

◆ push_state()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
bool spot::lpar13< State, SuccIterator, StateHash, StateEqual >::push_state ( product_state  ,
unsigned  dfsnum,
acc_cond::mark_t  cond 
)
inline

Push product state to stack.

◆ result()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
mc_rvalue spot::lpar13< State, SuccIterator, StateHash, StateEqual >::result ( )
inline

Return emptiness check result.

References spot::EMPTY, and spot::NOT_EMPTY.

◆ run()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
bool spot::lpar13< State, SuccIterator, StateHash, StateEqual >::run ( )
inline

Run the algorithm.

◆ sccs()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
int spot::lpar13< State, SuccIterator, StateHash, StateEqual >::sccs ( )
inline

Return number of SCCs found.

◆ setup()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
void spot::lpar13< State, SuccIterator, StateHash, StateEqual >::setup ( )
inline

Setup thread resources.

◆ states()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
unsigned int spot::lpar13< State, SuccIterator, StateHash, StateEqual >::states ( )
inline

Return number of states visited.

◆ trace()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
std::string spot::lpar13< State, SuccIterator, StateHash, StateEqual >::trace ( )
inline

Return trace.

◆ transitions()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
unsigned int spot::lpar13< State, SuccIterator, StateHash, StateEqual >::transitions ( )
inline

Return number of transitions traversed.

◆ update()

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.

◆ walltime()

template<typename State , typename SuccIterator , typename StateHash , typename StateEqual >
unsigned spot::lpar13< State, SuccIterator, StateHash, StateEqual >::walltime ( )
inline

Return wall time in milliseconds.

The documentation for this class was generated from the following file:
Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1