spot::ta_explicit Class Reference

#include <spot/ta/taexplicit.hh>

Inheritance diagram for spot::ta_explicit:

Collaboration diagram for spot::ta_explicit:

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_explicit (const const_twa_ptr &tgba, unsigned n_acc, state_ta_explicit *artificial_initial_state=nullptr)
const_twa_ptr	get_tgba () const
state_ta_explicit *	add_state (state_ta_explicit *s)
void	add_to_initial_states_set (state *s, bdd condition=bddfalse)
void	create_transition (state_ta_explicit *source, bdd condition, acc_cond::mark_t acceptance_conditions, const state_ta_explicit *dest, bool add_at_beginning=false)
void	delete_stuttering_transitions ()
virtual const_states_set_t	get_initial_states_set () const override
	Get the initial states set of the automaton. More...
virtual ta_succ_iterator *	succ_iter (const spot::state *s) const override
	Get an iterator over the successors of state. More...
virtual ta_succ_iterator *	succ_iter (const spot::state *s, bdd condition) 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...
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...
virtual spot::state *	get_artificial_initial_state () const override
	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...
void	set_artificial_initial_state (state_ta_explicit *s)
void	delete_stuttering_and_hole_successors (const spot::state *s)
ta::states_set_t	get_states_set ()
const acc_cond &	acc () const
acc_cond &	acc ()

Protected Attributes
acc_cond	acc_
bdd_dict_ptr	dict_

Detailed Description

Explicit representation of a spot::ta.

Member Function Documentation

format_state()

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

overridevirtual

Format the state as a string for printing.

This formatting is the responsibility of the automata that owns the state.

Implements spot::ta.

free_state()

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

overridevirtual

Release a state s.

Implements spot::ta.

get_artificial_initial_state()

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

inlineoverridevirtual

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 from spot::ta.

get_initial_states_set()

virtual const_states_set_t spot::ta_explicit::get_initial_states_set ( ) const

overridevirtual

Get the initial states set of the automaton.

Implements spot::ta.

get_state_condition()

virtual bdd spot::ta_explicit::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_explicit::is_accepting_state ( const spot::state *  s ) const

overridevirtual

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

Implements spot::ta.

is_initial_state()

virtual bool spot::ta_explicit::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_explicit::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 * spot::ta_explicit::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 responsibility of the caller to delete it when no longer needed.

Implements spot::ta.

succ_iter() [2/2]

virtual ta_succ_iterator * spot::ta_explicit::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 responsibility 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/taexplicit.hh