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

using	shared_struct = int

Public Member Functions
	lpar13 (kripkecube< State, SuccIterator > &sys, twacube_ptr twa, shared_map &map, shared_struct *, unsigned tid, std::atomic< bool > &stop)

bool	run ()

void	setup ()

bool	push_state (product_state, unsigned dfsnum, acc_cond::mark_t cond)

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 return 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 inconsistency 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. Return true if a counterexample has been found. More...

void	finalize ()

bool	finisher ()

unsigned int	states ()

unsigned int	transitions ()

unsigned	walltime ()

std::string	name ()

int	sccs ()

mc_rvalue	result ()

std::string	trace ()

Static Public Member Functions
static shared_struct *	make_shared_structure (shared_map m, unsigned i)

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 Function Documentation

◆ 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 return 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 inconsistency values.

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

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

spot/mc/lpar13.hh

Public Types

Public Member Functions

Static Public Member Functions

Detailed Description

Member Function Documentation

◆ pop_state()

◆ update()