spot::ta_check Class Reference

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.
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.
std::ostream &	print_stats (std::ostream &os) const
	Print statistics, if any.
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.
option_map	o_
	The options.
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 [geldenhuys.06.spin] .

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