Check whether the language of a product (spot::ta_product) between a Kripke structure and a TA is empty. It works also for the product using Generalized TA (GTA and SGTA). More...

#include <spot/taalgos/emptinessta.hh>

Inheritance diagram for spot::ta_check:

Collaboration diagram for spot::ta_check:

Public Types
typedef unsigned(unsigned_statistics::*	unsigned_fun) () const

typedef std::map< const char *, unsigned_fun, char_ptr_less_than >	stats_map

Public Member Functions
	ta_check (const const_ta_product_ptr &a, option_map o=option_map())

bool	check (bool disable_second_pass=false, bool disable_heuristic_for_livelock_detection=false)
	Check whether the TA product automaton contains an accepting run: it detects the two kinds of accepting runs: Buchi-accepting runs and livelock-accepting runs. This emptiness check algorithm can also check a product using the generalized form of TA. More...

bool	livelock_detection (const const_ta_product_ptr &t)
	Check whether the product automaton contains a livelock-accepting run Return false if the product automaton accepts no livelock-accepting run, otherwise true. More...

std::ostream &	print_stats (std::ostream &os) const
	Print statistics, if any. More...

void	set_states (unsigned n)

void	inc_states ()

void	inc_transitions ()

void	inc_depth (unsigned n=1)

void	dec_depth (unsigned n=1)

unsigned	states () const

unsigned	transitions () const

unsigned	max_depth () const

unsigned	depth () const

unsigned	get (const char *str) const

Public Attributes
stats_map	stats

Protected Member Functions
void	clear (hash_type &h, std::stack< pair_state_iter > todo, std::queue< const spot::state * > init_set)

void	clear (hash_type &h, std::stack< pair_state_iter > todo, spot::ta_succ_iterator *init_states_it)

bool	heuristic_livelock_detection (const state stuttering_succ, hash_type &h, int h_livelock_root, std::set< const state , state_ptr_less_than > liveset_curr)

Protected Attributes
const_ta_product_ptr	a_
	The automaton. More...

option_map	o_
	The options. More...

bool	is_full_2_pass_

scc_stack_ta	scc

scc_stack_ta	sscc

Detailed Description

Check whether the language of a product (spot::ta_product) between a Kripke structure and a TA is empty. It works also for the product using Generalized TA (GTA and SGTA).

you should call spot::ta_check::check() to check the product automaton. If spot::ta_check::check() returns false, then the product automaton was found empty. Otherwise the automaton accepts some run.

This is based on [24] .

the implementation of spot::ta_check::check() is inspired from the two-pass algorithm of the paper above:

the fist-pass detect all Buchi-accepting cycles and includes the heuristic proposed in the paper to detect some livelock-accepting cycles.
the second-pass detect all livelock-accepting cycles. In addition, we add some optimizations to the fist pass: 1- Detection of all cycles containing a least one state that is both livelock and Buchi accepting states 2- Detection of all livelock-accepting cycles containing a least one state (k,t) such as its "TA component" t is a livelock-accepting state that has no successors in the TA automaton.

The implementation of the algorithm of each pass is a SCC-based algorithm inspired from spot::gtec.hh.

An implementation of the emptiness-check algorithm for a product between a TA and a Kripke structure

See the paper cited above.

Member Function Documentation

◆ check()

bool spot::ta_check::check	(	bool	disable_second_pass = `false`,
		bool	disable_heuristic_for_livelock_detection = `false`
	)

Check whether the TA product automaton contains an accepting run: it detects the two kinds of accepting runs: Buchi-accepting runs and livelock-accepting runs. This emptiness check algorithm can also check a product using the generalized form of TA.

Return false if the product automaton accepts no run, otherwise true

Parameters

disable_second_pass	is used to disable the second pass when when it is not necessary, for example when all the livelock-accepting states of the TA automaton have no successors, we call this kind of TA as STA (Single-pass Testing Automata) (see spot::tgba2ta::add_artificial_livelock_accepting_state() for an automatic transformation of any TA automaton into STA automaton
disable_heuristic_for_livelock_detection	disable the heuristic used in the first pass to detect livelock-accepting runs, this heuristic is described in the paper cited above

◆ heuristic_livelock_detection()

bool spot::ta_check::heuristic_livelock_detection	(	const state *	stuttering_succ,
		hash_type &	h,
		int	h_livelock_root,
		std::set< const state *, state_ptr_less_than >	liveset_curr
	)

protected

the heuristic for livelock-accepting runs detection, it's described in the paper cited above

◆ livelock_detection()

bool spot::ta_check::livelock_detection ( const const_ta_product_ptr & t )

Check whether the product automaton contains a livelock-accepting run Return false if the product automaton accepts no livelock-accepting run, otherwise true.

◆ print_stats()

std::ostream& spot::ta_check::print_stats ( std::ostream & os ) const

Print statistics, if any.

Member Data Documentation

◆ a_

const_ta_product_ptr spot::ta_check::a_

protected

The automaton.

◆ o_

option_map spot::ta_check::o_

protected

The options.

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

spot/taalgos/emptinessta.hh

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Function Documentation

◆ check()

◆ heuristic_livelock_detection()

◆ livelock_detection()

◆ print_stats()

Member Data Documentation

◆ a_

◆ o_