spot::ta_product Class Reference

A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly.) More...

#include <spot/ta/taproduct.hh>

Inheritance diagram for spot::ta_product:

Collaboration diagram for spot::ta_product:

Public Types
typedef std::set< state *, state_ptr_less_than >	states_set_t
typedef std::set< const state *, state_ptr_less_than >	const_states_set_t

Public Member Functions
	ta_product (const const_ta_ptr &testing_automaton, const const_kripke_ptr &kripke_structure)
	Constructor. More...
virtual ta::const_states_set_t	get_initial_states_set () const override
	Get the initial states set of the automaton. More...
virtual ta_succ_iterator_product *	succ_iter (const spot::state *s) const override
	Get an iterator over the successors of state. More...
virtual ta_succ_iterator_product *	succ_iter (const spot::state *s, bdd changeset) const override
	Get an iterator over the successors of state filtred by the changeset on transitions. More...
bdd_dict_ptr	get_dict () const
virtual std::string	format_state (const spot::state *s) const override
	Format the state as a string for printing. More...
virtual bool	is_accepting_state (const spot::state *s) const override
	Return true if s is a Buchi-accepting state, otherwise false. More...
virtual bool	is_livelock_accepting_state (const spot::state *s) const override
	Return true if s is a livelock-accepting state , otherwise false. More...
virtual bool	is_initial_state (const spot::state *s) const override
	Return true if s is an initial state, otherwise false. More...
bool	is_hole_state_in_ta_component (const spot::state *s) const
	Return true if the state s has no succeseurs in the TA automaton (the TA component of the product automaton) More...
virtual bdd	get_state_condition (const spot::state *s) const override
	Return a BDD condition that represents the valuation of atomic propositions in the state s. More...
virtual void	free_state (const spot::state *s) const override
	Release a state s. More...
const const_ta_ptr &	get_ta () const
const const_kripke_ptr &	get_kripke () const
virtual const spot::state *	get_artificial_initial_state () const
	Get the artificial initial state set of the automaton. Return 0 if this artificial state is not implemented (in this case, use get_initial_states_set) The aim of adding this state is to have a unique initial state. This artificial initial state have one transition to each real initial state, and this transition is labeled by the corresponding initial condition. (For more details, see the paper cited above) More...
const acc_cond &	acc () const
acc_cond &	acc ()

Protected Attributes
acc_cond	acc_

Detailed Description

A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly.)

Constructor & Destructor Documentation

ta_product()

spot::ta_product::ta_product	(	const const_ta_ptr &	testing_automaton,
		const const_kripke_ptr &	kripke_structure
	)

Constructor.

Parameters

testing_automaton	The TA component in the product.
kripke_structure	The Kripke component in the product.

Member Function Documentation

format_state()

virtual std::string spot::ta_product::format_state ( const spot::state *  s ) const

overridevirtual

Format the state as a string for printing.

This formating is the responsability of the automata that owns the state.

Implements spot::ta.

free_state()

virtual void spot::ta_product::free_state ( const spot::state *  s ) const

overridevirtual

Release a state s.

Implements spot::ta.

get_artificial_initial_state()

virtual const spot::state* spot::ta::get_artificial_initial_state ( ) const

inlinevirtualinherited

Get the artificial initial state set of the automaton. Return 0 if this artificial state is not implemented (in this case, use get_initial_states_set) The aim of adding this state is to have a unique initial state. This artificial initial state have one transition to each real initial state, and this transition is labeled by the corresponding initial condition. (For more details, see the paper cited above)

Reimplemented in spot::ta_explicit.

get_initial_states_set()

virtual ta::const_states_set_t spot::ta_product::get_initial_states_set ( ) const

overridevirtual

Get the initial states set of the automaton.

Implements spot::ta.

get_state_condition()

virtual bdd spot::ta_product::get_state_condition ( const spot::state *  s ) const

overridevirtual

Return a BDD condition that represents the valuation of atomic propositions in the state s.

Implements spot::ta.

is_accepting_state()

virtual bool spot::ta_product::is_accepting_state ( const spot::state *  s ) const

overridevirtual

Return true if s is a Buchi-accepting state, otherwise false.

Implements spot::ta.

is_hole_state_in_ta_component()

bool spot::ta_product::is_hole_state_in_ta_component

(

const spot::state *

s

)

const

Return true if the state s has no succeseurs in the TA automaton (the TA component of the product automaton)

is_initial_state()

virtual bool spot::ta_product::is_initial_state ( const spot::state *  s ) const

overridevirtual

Return true if s is an initial state, otherwise false.

Implements spot::ta.

is_livelock_accepting_state()

virtual bool spot::ta_product::is_livelock_accepting_state ( const spot::state *  s ) const

overridevirtual

Return true if s is a livelock-accepting state , otherwise false.

Implements spot::ta.

succ_iter() [1/2]

virtual ta_succ_iterator_product* spot::ta_product::succ_iter ( const spot::state *  state ) const

overridevirtual

Get an iterator over the successors of state.

The iterator has been allocated with new. It is the responsability of the caller to delete it when no longer needed.

Implements spot::ta.

succ_iter() [2/2]

virtual ta_succ_iterator_product* spot::ta_product::succ_iter ( const spot::state *  state, bdd  changeset  ) const

overridevirtual

Get an iterator over the successors of state filtred by the changeset on transitions.

The iterator has been allocated with new. It is the responsability of the caller to delete it when no longer needed.

Implements spot::ta.

---

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

• spot/ta/taproduct.hh