spot::twa_graph Class Reference

Graph-based representation of a TωA. More...

#include <spot/twa/twagraph.hh>

Inheritance diagram for spot::twa_graph:

Collaboration diagram for spot::twa_graph:

Public Types
typedef digraph< twa_graph_state, twa_graph_edge_data >	graph_t
	The underlying graph type.
typedef spot::internal::edge_storage< unsigned, unsigned, unsigned, internal::boxed_label< twa_graph_edge_data, false > >	edge_storage_t
	Edge storage type (src, dst, and edge data).
typedef unsigned	state_num
	Numeric type used to identify states.
template<typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>
using	namer = named_graph< graph_t, State_Name, Name_Hash, Name_Equal >
	Template alias for a helper that names graph states.
typedef void(*	shift_action) (const std::vector< unsigned > &newst, void *action_data)
	Remove all unreachable states.

Public Member Functions
	twa_graph (const bdd_dict_ptr &dict)
	Construct an empty automaton using dict for BDD variables.
	twa_graph (const const_twa_graph_ptr &other, prop_set p)
	Copy another automaton, keeping only the properties in p.
template<typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>
namer< State_Name, Name_Hash, Name_Equal > *	create_namer ()
	Create a namer to associate custom names of type State_Name to states.
namer< formula > *	create_formula_namer ()
	Create a namer that associates formulas to states.
void	release_formula_namer (namer< formula > *namer, bool keep_names)
	Release a formula namer.
graph_t &	get_graph ()
	Access the underlying digraph.
const graph_t &	get_graph () const
	Access the underlying digraph (const overload).
unsigned	num_states () const
	Returns the number of states in the automaton.
unsigned	num_edges () const
	Returns the number of edges in the automaton.
void	set_init_state (state_num s)
	Set the initial state to state number s.
template<class I >
void	set_univ_init_state (I dst_begin, I dst_end)
	Set a universal initial state from a range of destination states.
void	set_univ_init_state (const std::initializer_list< state_num > &il)
	Set a universal initial state from an initializer list.
state_num	get_init_state_number () const
	Returns the number of the initial state.
virtual const twa_graph_state *	get_init_state () const override
	Get the initial state of the automaton.
virtual twa_succ_iterator *	succ_iter (const state *st) const override
	Get an iterator over the successors of local_state.
state_num	state_number (const state *st) const
	Returns the state number corresponding to state pointer st.
const twa_graph_state *	state_from_number (state_num n) const
	Returns the state pointer for state number n.
std::string	format_state (unsigned n) const
	Returns a human-readable representation of state number n.
virtual std::string	format_state (const state *st) const override
	Format the state as a string for printing.
unsigned	edge_number (const twa_succ_iterator *it) const
	Returns the index of the current edge of iterator it.
unsigned	edge_number (const edge_storage_t &e) const
	Returns the index of edge e.
twa_graph_edge_data &	edge_data (const twa_succ_iterator *it)
	Returns the edge data at the current position of iterator it.
twa_graph_edge_data &	edge_data (unsigned t)
	Returns the edge data for edge number t.
const twa_graph_edge_data &	edge_data (const twa_succ_iterator *it) const
	Returns the edge data at the position of iterator it (const).
const twa_graph_edge_data &	edge_data (unsigned t) const
	Returns the edge data for edge number t (const overload).
edge_storage_t &	edge_storage (const twa_succ_iterator *it)
	Returns the edge storage at the position of iterator it.
edge_storage_t &	edge_storage (unsigned t)
	Returns the edge storage for edge number t.
const edge_storage_t	edge_storage (const twa_succ_iterator *it) const
	Returns edge storage at the position of iterator it (const).
const edge_storage_t	edge_storage (unsigned t) const
	Returns edge storage for edge number t (const overload).
unsigned	new_state ()
	Create a new state and return its number.
unsigned	new_states (unsigned n)
	Create n new states; return the number of the first one.
unsigned	new_edge (unsigned src, unsigned dst, bdd cond, acc_cond::mark_t acc={})
	Create a new edge from src to dst.
unsigned	new_acc_edge (unsigned src, unsigned dst, bdd cond, bool acc=true)
	Create an edge from src to dst.
template<class I >
unsigned	new_univ_edge (unsigned src, I begin, I end, bdd cond, acc_cond::mark_t acc={})
	Create a universal edge from src to states in [begin, end).
unsigned	new_univ_edge (unsigned src, std::initializer_list< unsigned > dst, bdd cond, acc_cond::mark_t acc={})
	Create a universal edge from src to the listed destinations.
internal::state_out< const graph_t >	out (unsigned src) const
	Returns a range over outgoing edges of state src (const).
internal::state_out< graph_t >	out (unsigned src)
	Returns a range over outgoing edges of state src.
internal::killer_edge_iterator< graph_t >	out_iteraser (unsigned src)
	Returns an edge-erasing iterator over outgoing edges of src.
internal::const_universal_dests	univ_dests (unsigned d) const noexcept
	Returns the universal destinations of dest-index d.
internal::const_universal_dests	univ_dests (const edge_storage_t &e) const noexcept
	Returns the universal destinations of edge e.
bool	is_existential () const
	Whether the automaton uses only existential branching.
auto	states () const SPOT_RETURN(g_.states())
	Returns a range over all states (const).
auto	states () SPOT_RETURN(g_.states())
	Returns a range over all states.
internal::all_trans< const graph_t >	edges () const noexcept
	Returns a range over all edges (const).
internal::all_trans< graph_t >	edges () noexcept
	Returns a range over all edges.
auto	edge_vector () const SPOT_RETURN(g_.edge_vector())
	Returns the raw edge storage vector (const).
auto	edge_vector () SPOT_RETURN(g_.edge_vector())
	Returns the raw edge storage vector.
bool	is_dead_edge (unsigned t) const
	Returns true iff edge number t is a dead (removed) edge.
bool	is_dead_edge (const graph_t::edge_storage_t &t) const
	Returns true iff edge t is a dead (removed) edge.
void	merge_edges ()
	Merge edges that can be merged.
void	merge_univ_dests ()
	Merge common universal destinations.
unsigned	merge_states (parallel_policy ppolicy=parallel_policy())
	Merge states that can be merged.
unsigned	merge_states_of (bool stable=true, const std::vector< bool > *to_merge_ptr=nullptr)
	Like merge states, but one can chose which states are candidates for merging.
void	purge_dead_states ()
	Remove all dead states.
void	purge_unreachable_states (shift_action *f=nullptr, void *action_data=nullptr)
	Remove all unreachable states.
void	remove_unused_ap ()
	Remove unused atomic propositions.
void	copy_state_names_from (const const_twa_graph_ptr &other)
	Define the state names of this automaton using the names from other.
acc_cond::mark_t	state_acc_sets (unsigned s) const
	Return the marks associated to a state if the acceptance is state-based.
bool	operator== (const twa_graph &aut) const
	Structural equality: same states, edges, labels, and acceptance.
void	kill_state (unsigned state)
	Make a state dead.
void	dump_storage_as_dot (std::ostream &out, const char *opt=nullptr) const
	Print the data structures used to represent the automaton in dot's format.
internal::twa_succ_iterable	succ (const state *s) const
	Build an iterable over the successors of s.
void	release_iter (twa_succ_iterator *i) const
	Release an iterator after usage.
bdd_dict_ptr	get_dict () const
	Get the dictionary associated to the automaton.
void	unregister_ap (int num)
	Unregister an atomic proposition.
void	register_aps_from_dict ()
	Register all atomic propositions that have already been registered by the bdd_dict for this automaton.
const std::vector< formula > &	ap () const
	The vector of atomic propositions registered by this automaton.
bdd	ap_vars () const
	The set of atomic propositions as a conjunction.
virtual state *	project_state (const state *s, const const_twa_ptr &t) const
	Project a state on an automaton.
virtual bool	is_empty () const
	Check whether the language of the automaton is empty.
virtual twa_run_ptr	accepting_run () const
	Return an accepting run if one exists.
virtual twa_word_ptr	accepting_word () const
	Return an accepting word if one exists.
virtual bool	intersects (const_twa_ptr other) const
	Check whether the language of this automaton intersects that of the other automaton.
virtual bool	intersects (const_twa_word_ptr w) const
	Check if this automaton _word intersects a word.
virtual twa_run_ptr	intersecting_run (const_twa_ptr other) const
	Return an accepting run recognizing a word accepted by two automata.
virtual twa_word_ptr	intersecting_word (const_twa_ptr other) const
	Return a word accepted by two automata.
virtual twa_run_ptr	exclusive_run (const_twa_ptr other) const
	Return an accepting run recognizing a word accepted by exactly one of the two automata.
virtual twa_word_ptr	exclusive_word (const_twa_ptr other) const
	Return a word accepted by exactly one of the two automata.
unsigned	num_sets () const
	Number of acceptance sets used by the automaton.
const acc_cond::acc_code &	get_acceptance () const
	Acceptance formula used by the automaton.
void	set_acceptance (unsigned num, const acc_cond::acc_code &c)
	Set the acceptance condition of the automaton.
void	set_acceptance (const acc_cond &c)
	Set the acceptance condition of the automaton.
void	copy_acceptance_of (const const_twa_ptr &a)
	Copy the acceptance condition of another TωA.
void	copy_ap_of (const const_twa_ptr &a)
	Copy the atomic propositions of another TωA.
void	copy_named_properties_of (const const_twa_ptr &a)
	Copy all the named properties of a into this automaton.
void	set_generalized_buchi (unsigned num)
	Set generalized Büchi acceptance.
void	set_generalized_co_buchi (unsigned num)
	Set generalized co-Büchi acceptance.
acc_cond::mark_t	set_buchi ()
	Set Büchi acceptance.
acc_cond::mark_t	set_co_buchi ()
	Set co-Büchi acceptance.
void	set_named_prop (std::string s, void *val, std::function< void(void *)> destructor)
	Declare a named property.
template<typename T >
void	set_named_prop (std::string s, T *val)
	Declare a named property.
void	set_named_prop (std::string s, std::nullptr_t)
	Erase a named property.
template<typename T >
T *	get_named_prop (std::string s) const
	Retrieve a named property.
template<typename T >
T *	get_or_set_named_prop (std::string s)
	Create or retrieve a named property.
void	release_named_properties ()
	Destroy all named properties.
trival	prop_state_acc () const
	Whether the automaton uses state-based acceptance.
void	prop_state_acc (trival val)
	Set the state-based-acceptance property.
trival	is_sba () const
	Whether this is a state-based Büchi automaton.
trival	prop_inherently_weak () const
	Whether the automaton is inherently weak.
void	prop_inherently_weak (trival val)
	Set the "inherently weak" property.
trival	prop_terminal () const
	Whether the automaton is terminal.
void	prop_terminal (trival val)
	Set the terminal property.
trival	prop_weak () const
	Whether the automaton is weak.
void	prop_weak (trival val)
	Set the weak property.
trival	prop_very_weak () const
	Whether the automaton is very-weak.
void	prop_very_weak (trival val)
	Set the very-weak property.
trival	prop_complete () const
	Whether the automaton is complete.
void	prop_complete (trival val)
	Set the complete property.
trival	prop_universal () const
	Whether the automaton is universal.
void	prop_universal (trival val)
	Set the universal property.
trival	prop_unambiguous () const
	Whether the automaton is unambiguous.
void	prop_unambiguous (trival val)
	Set the unambiguous property.
trival	prop_semi_deterministic () const
	Whether the automaton is semi-deterministic.
void	prop_semi_deterministic (trival val)
	Set the semi-deterministic property.
trival	prop_stutter_invariant () const
	Whether the automaton is stutter-invariant.
void	prop_stutter_invariant (trival val)
	Set the stutter-invariant property.
void	prop_copy (const const_twa_ptr &other, prop_set p)
	Copy the properties of another automaton.
void	prop_keep (prop_set p)
	Keep only a subset of properties of the current automaton.
void	prop_reset ()
	Reset all automaton properties to trival::maybe().
bool	state_is_accepting (unsigned s) const
	Tell if a state is accepting.
bool	state_is_accepting (const state *s) const
	Tell if a state is accepting.
void	defrag_states (std::vector< unsigned > &newst, unsigned used_states)
	Renumber all states, and drop some.
void	defrag_states (std::vector< unsigned > &&newst, unsigned used_states)
	Renumber all states, and drop some.
void	rename_states_ (const std::vector< unsigned > &newst)
	Rename all states.
int	register_ap (formula ap)
	Register an atomic proposition designated by ap.
int	register_ap (std::string ap)
	Register an atomic proposition designated by ap.
const acc_cond &	acc () const
	The acceptance condition of the automaton.
acc_cond &	acc ()
	The acceptance condition of the automaton.

Static Public Member Functions
static constexpr bool	is_univ_dest (const edge_storage_t &e)
	Returns true iff edge e has a universal destination.
static constexpr bool	is_univ_dest (unsigned s)
	Returns true iff destination s is a universal destination.

Protected Member Functions
void *	get_named_prop_ (std::string s) const
	Look up a named property by name.

Protected Attributes
graph_t	g_
	The underlying graph.
unsigned	init_number_
	Number of the initial state.
twa_succ_iterator *	iter_cache_
	Any iterator returned via release_iter.
bdd_dict_ptr	dict_
	BDD dictionary used by the automaton.
std::unordered_map< std::string, std::pair< void *, std::function< void(void *)> > >	named_prop_
	Storage for named properties.

Detailed Description

Graph-based representation of a TωA.

Member Typedef Documentation

edge_storage_t

typedef spot::internal::edge_storage<unsigned, unsigned, unsigned, internal::boxed_label <twa_graph_edge_data, false> > spot::twa_graph::edge_storage_t

Edge storage type (src, dst, and edge data).

graph_t

typedef digraph<twa_graph_state, twa_graph_edge_data> spot::twa_graph::graph_t

The underlying graph type.

namer

template<typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

using spot::twa_graph::namer = named_graph<graph_t, State_Name, Name_Hash, Name_Equal>

Template alias for a helper that names graph states.

shift_action

typedef void(* spot::twa_graph::shift_action) (const std::vector< unsigned > &newst, void *action_data)

Remove all unreachable states.

A state is unreachable if it cannot be reached from the initial state.

Use this function if you have declared more states than you actually need in the automaton. It runs in linear time.

purge_dead_states() will remove more states than purge_unreachable_states(), but it is more costly.

You can pass a function to this method, which will be invoked with a vector indicating the renumbering of states. newst[i] == -1U means that state i is unreachable and thus deleted. Otherwise, state i is renumbered newst[i].

See also

purge_dead_states

state_num

typedef unsigned spot::twa_graph::state_num

Numeric type used to identify states.

Constructor & Destructor Documentation

twa_graph() [1/2]

spot::twa_graph::twa_graph ( const bdd_dict_ptr &  dict )

inline

Construct an empty automaton using dict for BDD variables.

twa_graph() [2/2]

spot::twa_graph::twa_graph ( const const_twa_graph_ptr &  other, prop_set  p  )

inlineexplicit

Copy another automaton, keeping only the properties in p.

Member Function Documentation

acc() [1/2]

acc_cond & spot::twa::acc ( )

inlineinherited

The acceptance condition of the automaton.

acc() [2/2]

const acc_cond & spot::twa::acc ( ) const

inlineinherited

The acceptance condition of the automaton.

accepting_run()

virtual twa_run_ptr spot::twa::accepting_run ( ) const

virtualinherited

Return an accepting run if one exists.

Return nullptr if no accepting run were found.

If you are calling this method on a product of two automata, consider using intersecting_run() instead.

Note that if the input automaton uses Fin-acceptance, this computation is not performed on-the-fly. Any on-the-fly automaton would be automatically copied into a twa_graph_ptr first.

accepting_word()

virtual twa_word_ptr spot::twa::accepting_word ( ) const

virtualinherited

Return an accepting word if one exists.

Return nullptr if no accepting word were found.

If you are calling this method on a product of two automata, consider using intersecting_word() instead.

Note that if the input automaton uses Fin-acceptance, this computation is not performed on-the-fly. Any on-the-fly automaton would be automatically copied into a twa_graph_ptr first.

ap()

const std::vector< formula > & spot::twa::ap ( ) const

inlineinherited

The vector of atomic propositions registered by this automaton.

ap_vars()

bdd spot::twa::ap_vars ( ) const

inlineinherited

The set of atomic propositions as a conjunction.

copy_acceptance_of()

void spot::twa::copy_acceptance_of ( const const_twa_ptr &  a )

inlineinherited

Copy the acceptance condition of another TωA.

copy_ap_of()

void spot::twa::copy_ap_of ( const const_twa_ptr &  a )

inlineinherited

Copy the atomic propositions of another TωA.

copy_named_properties_of()

void spot::twa::copy_named_properties_of ( const const_twa_ptr &  a )

inherited

Copy all the named properties of a into this automaton.

copy_state_names_from()

void spot::twa_graph::copy_state_names_from

(

const const_twa_graph_ptr &

other

)

Define the state names of this automaton using the names from other.

If the "original-states" named property is set, it is used to map the state numbers, otherwise an identity mapping is assumed.

create_formula_namer()

namer< formula > * spot::twa_graph::create_formula_namer ( )

inline

Create a namer that associates formulas to states.

create_namer()

template<typename State_Name , typename Name_Hash = std::hash<State_Name>, typename Name_Equal = std::equal_to<State_Name>>

namer< State_Name, Name_Hash, Name_Equal > * spot::twa_graph::create_namer ( )

inline

Create a namer to associate custom names of type State_Name to states.

defrag_states() [1/2]

void spot::twa_graph::defrag_states ( std::vector< unsigned > &&  newst, unsigned  used_states  )

inline

Renumber all states, and drop some.

This semi-internal function is a wrapper around digraph::defrag_state() that additionally deals with universal branching.

This method is used to remove some states that have been previously detected to be unreachable in order to "defragment" the state vector. When a state is removed, all its outgoing transition are removed as well. Removing reachable states should NOT be attempted, because the incoming edges will be dangling.

Parameters

newst	A vector indicating how each state should be renumbered. Use -1U to mark an unreachable state for removal. Ignoring the occurrences of -1U. If the automaton contains universal branching, this vector is likely to be modified by this function, so do not reuse it afterwards.
used_states	the number of states used after renumbering.

defrag_states() [2/2]

void spot::twa_graph::defrag_states	(	std::vector< unsigned > &	newst,
		unsigned	used_states
	)

Renumber all states, and drop some.

This semi-internal function is a wrapper around digraph::defrag_state() that additionally deals with universal branching.

This method is used to remove some states that have been previously detected to be unreachable in order to "defragment" the state vector. When a state is removed, all its outgoing transition are removed as well. Removing reachable states should NOT be attempted, because the incoming edges will be dangling.

Parameters

newst	A vector indicating how each state should be renumbered. Use -1U to mark an unreachable state for removal. Ignoring the occurrences of -1U. If the automaton contains universal branching, this vector is likely to be modified by this function, so do not reuse it afterwards.
used_states	the number of states used after renumbering.

dump_storage_as_dot()

void spot::twa_graph::dump_storage_as_dot	(	std::ostream &	out,
		const char *	opt = nullptr
	)		const

Print the data structures used to represent the automaton in dot's format.

opt should be a substring of "vdp" if you want to print only the vectors, data, or properties.

edge_data() [1/4]

twa_graph_edge_data & spot::twa_graph::edge_data ( const twa_succ_iterator *  it )

inline

Returns the edge data at the current position of iterator it.

References spot::digraph< State_Data, Edge_Data >::edge_data().

edge_data() [2/4]

const twa_graph_edge_data & spot::twa_graph::edge_data ( const twa_succ_iterator *  it ) const

inline

Returns the edge data at the position of iterator it (const).

References spot::digraph< State_Data, Edge_Data >::edge_data().

edge_data() [3/4]

twa_graph_edge_data & spot::twa_graph::edge_data ( unsigned  t )

inline

Returns the edge data for edge number t.

References spot::digraph< State_Data, Edge_Data >::edge_data().

edge_data() [4/4]

const twa_graph_edge_data & spot::twa_graph::edge_data ( unsigned  t ) const

inline

Returns the edge data for edge number t (const overload).

References spot::digraph< State_Data, Edge_Data >::edge_data().

edge_number() [1/2]

unsigned spot::twa_graph::edge_number ( const edge_storage_t &  e ) const

inline

Returns the index of edge e.

References spot::digraph< State_Data, Edge_Data >::index_of_edge().

edge_number() [2/2]

unsigned spot::twa_graph::edge_number ( const twa_succ_iterator *  it ) const

inline

Returns the index of the current edge of iterator it.

edge_storage() [1/4]

edge_storage_t & spot::twa_graph::edge_storage ( const twa_succ_iterator *  it )

inline

Returns the edge storage at the position of iterator it.

References spot::digraph< State_Data, Edge_Data >::edge_storage().

edge_storage() [2/4]

const edge_storage_t spot::twa_graph::edge_storage ( const twa_succ_iterator *  it ) const

inline

Returns edge storage at the position of iterator it (const).

References spot::digraph< State_Data, Edge_Data >::edge_storage().

edge_storage() [3/4]

edge_storage_t & spot::twa_graph::edge_storage ( unsigned  t )

inline

Returns the edge storage for edge number t.

References spot::digraph< State_Data, Edge_Data >::edge_storage().

edge_storage() [4/4]

const edge_storage_t spot::twa_graph::edge_storage ( unsigned  t ) const

inline

Returns edge storage for edge number t (const overload).

References spot::digraph< State_Data, Edge_Data >::edge_storage().

edge_vector() [1/2]

auto spot::twa_graph::edge_vector

(

)

const

Returns the raw edge storage vector (const).

Referenced by operator==().

edge_vector() [2/2]

auto spot::twa_graph::edge_vector

(

)

Returns the raw edge storage vector.

edges() [1/2]

internal::all_trans< const graph_t > spot::twa_graph::edges ( ) const

inlinenoexcept

Returns a range over all edges (const).

References spot::digraph< State_Data, Edge_Data >::edges().

edges() [2/2]

internal::all_trans< graph_t > spot::twa_graph::edges ( )

inlinenoexcept

Returns a range over all edges.

References spot::digraph< State_Data, Edge_Data >::edges().

exclusive_run()

virtual twa_run_ptr spot::twa::exclusive_run ( const_twa_ptr  other ) const

virtualinherited

Return an accepting run recognizing a word accepted by exactly one of the two automata.

Return nullptr iff the two automata recognize the same language.

This methods needs to complement at least one automaton (if lucky) or maybe both automata. It will therefore be more efficient on deterministic automata.

exclusive_word()

virtual twa_word_ptr spot::twa::exclusive_word ( const_twa_ptr  other ) const

virtualinherited

Return a word accepted by exactly one of the two automata.

Return nullptr iff the two automata recognize the same language.

This methods needs to complement at least one automaton (if lucky) or maybe both automata. It will therefore be more efficient on deterministic automata.

format_state() [1/2]

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

inlineoverridevirtual

Format the state as a string for printing.

Formatting is the responsibility of the automata that owns the state, so that state objects could be implemented as very small objects, maybe sharing data with other state objects via data structure stored in the automaton.

Implements spot::twa.

format_state() [2/2]

std::string spot::twa_graph::format_state

(

unsigned

n

)

const

Returns a human-readable representation of state number n.

get_acceptance()

const acc_cond::acc_code & spot::twa::get_acceptance ( ) const

inlineinherited

Acceptance formula used by the automaton.

References spot::acc_cond::get_acceptance().

get_dict()

bdd_dict_ptr spot::twa::get_dict ( ) const

inlineinherited

Get the dictionary associated to the automaton.

Automata are labeled by Boolean formulas over atomic propositions. These Boolean formulas are represented as BDDs. The dictionary allows to map BDD variables back to atomic propositions, and vice versa.

Usually automata that are involved in the same computations should share their dictionaries so that operations between BDDs of the two automata work naturally.

It is however possible to declare automata that use different sets of atomic propositions with different dictionaries. That way, a BDD variable associated to some atomic proposition in one automaton might be reused for another atomic proposition in the other automaton.

get_graph() [1/2]

graph_t & spot::twa_graph::get_graph ( )

inline

Access the underlying digraph.

Referenced by operator==().

get_graph() [2/2]

const graph_t & spot::twa_graph::get_graph ( ) const

inline

Access the underlying digraph (const overload).

get_init_state()

virtual const twa_graph_state * spot::twa_graph::get_init_state ( ) const

inlineoverridevirtual

Get the initial state of the automaton.

The state has been allocated with new. It is the responsibility of the caller to destroy it when no longer needed.

Implements spot::twa.

get_init_state_number()

state_num spot::twa_graph::get_init_state_number ( ) const

inline

Returns the number of the initial state.

get_named_prop()

template<typename T >

T * spot::twa::get_named_prop ( std::string  s ) const

inlineinherited

Retrieve a named property.

Because named property can be object of any type, retrieving the object requires knowing its type.

Parameters

s	the name of the object to retrieve

Template Parameters

T	the type of the object to retrieve

Note that the return is a pointer to T, so the type should not include the pointer.

Returns a nullptr if no such named property exists.

See https://spot.lrde.epita.fr/concepts.html#named-properties for a list of named properties used by Spot.

get_named_prop_()

void * spot::twa::get_named_prop_ ( std::string  s ) const

protectedinherited

Look up a named property by name.

Returns a void* to the stored value, or nullptr if not found. This is the untyped backend for get_named_prop<T>().

get_or_set_named_prop()

template<typename T >

T * spot::twa::get_or_set_named_prop ( std::string  s )

inlineinherited

Create or retrieve a named property.

Arbitrary objects can be attached to automata. Those are called named properties. They are used for instance to name all the states of an automaton.

This function creates a property object of a given type, and attaches it to name if no such property exists, or it returns the found object.

See https://spot.lrde.epita.fr/concepts.html#named-properties for a list of named properties used by Spot.

intersecting_run()

virtual twa_run_ptr spot::twa::intersecting_run ( const_twa_ptr  other ) const

virtualinherited

Return an accepting run recognizing a word accepted by two automata.

The run returned is a run from automaton this.

Return nullptr if no accepting run were found.

An emptiness check is performed on a product computed on-the-fly, unless some of the operands use Fin-acceptance: in this case an explicit product is performed.

intersecting_word()

virtual twa_word_ptr spot::twa::intersecting_word ( const_twa_ptr  other ) const

virtualinherited

Return a word accepted by two automata.

Return nullptr if no accepting word were found.

intersects() [1/2]

virtual bool spot::twa::intersects ( const_twa_ptr  other ) const

virtualinherited

Check whether the language of this automaton intersects that of the other automaton.

An emptiness check is performed on a product computed on-the-fly, unless some of the operands use Fin-acceptance: in this case an explicit product is performed.

intersects() [2/2]

virtual bool spot::twa::intersects ( const_twa_word_ptr  w ) const

virtualinherited

Check if this automaton _word intersects a word.

If the twa_word actually represent a word (i.e., if each Boolean formula that label its steps have a unique satisfying valuation), this is equivalent to a membership test.

is_dead_edge() [1/2]

bool spot::twa_graph::is_dead_edge ( const graph_t::edge_storage_t &  t ) const

inline

Returns true iff edge t is a dead (removed) edge.

References spot::digraph< State_Data, Edge_Data >::is_dead_edge().

is_dead_edge() [2/2]

bool spot::twa_graph::is_dead_edge ( unsigned  t ) const

inline

Returns true iff edge number t is a dead (removed) edge.

References spot::digraph< State_Data, Edge_Data >::is_dead_edge().

is_empty()

virtual bool spot::twa::is_empty ( ) const

virtualinherited

Check whether the language of the automaton is empty.

If you are calling this method on a product of two automata, consider using intersects() instead.

Note that if the input automaton uses Fin-acceptance, the emptiness check is not performed on-the-fly. Any on-the-fly automaton would be automatically copied into a twa_graph_ptr first.

is_existential()

bool spot::twa_graph::is_existential ( ) const

inline

Whether the automaton uses only existential branching.

References spot::digraph< State_Data, Edge_Data >::is_existential().

is_sba()

trival spot::twa::is_sba ( ) const

inlineinherited

Whether this is a state-based Büchi automaton.

An SBA has a Büchi acceptance, and should have its state-based acceptance property set.

is_univ_dest() [1/2]

static constexpr bool spot::twa_graph::is_univ_dest ( const edge_storage_t &  e )

inlinestaticconstexpr

Returns true iff edge e has a universal destination.

is_univ_dest() [2/2]

static constexpr bool spot::twa_graph::is_univ_dest ( unsigned  s )

inlinestaticconstexpr

Returns true iff destination s is a universal destination.

kill_state()

void spot::twa_graph::kill_state

(

unsigned

state

)

Make a state dead.

A state is dead if it has no successors. So this function simply erases all edges leaving state.

It can be used together with purge_dead_states() to remove a set of states from an automaton.

merge_edges()

void spot::twa_graph::merge_edges

(

)

Merge edges that can be merged.

This makes two passes over the automaton to reduce the number of edges with an identical pair of source and destination.

In the first pass, which is performed only on automata with Fin-less acceptance, edges with the same source, destination, and conditions are merged into a single edge whose set of acceptance marks is the intersection of the sets of the edges.

In the second pass, edges that share their source, destination, and acceptance marks are merged into a single edge whose condition is the disjunction of the conditions of the original edges.

If the automaton uses some universal edges, the method merge_univ_dests() is also called.

merge_states()

unsigned spot::twa_graph::merge_states

(

parallel_policy

ppolicy = parallel_policy()

)

Merge states that can be merged.

Two states can be merged if the set of outgoing transitions is identical, i.e., same condition, same colors, same destination. Two self-loops with the same condition and colors are considered identical even if they do not actually have the same destination.

The implementation will sort the edges of the automaton to ease the comparison between two states. This may miss some self-loop equivalences in non-deterministic automata.

States whose input have been redirected as a consequence of a merge are removed from the automaton. This procedure therefore renumber states.

Merging states might create duplicate transitions in the automaton. For instance (1)-a->(2) and (1)-a->(3) will become (1)-a->(1) and (1)-a->(1) if (1), (2) and (3) are merged into (1).

On large automaton, it might be worthwhile to use multiple threads to find states that can be merged. This can be requested with the ppolicy argument.

Returns

the number of states that have been merged and removed.

merge_states_of()

unsigned spot::twa_graph::merge_states_of	(	bool	stable = true,
		const std::vector< bool > *	to_merge_ptr = nullptr
	)

Like merge states, but one can chose which states are candidates for merging.

Parameters

stable	Determines whether or not a stable sorting is used for the edges
to_merge_ptr	Determines which states are candidates. If null, all states are considered The actual implementation differs from merge_states(). It is more costly, but is more precise, in the sense that more states are merged.

merge_univ_dests()

void spot::twa_graph::merge_univ_dests

(

)

Merge common universal destinations.

This is already called by merge_edges().

new_acc_edge()

unsigned spot::twa_graph::new_acc_edge ( unsigned  src, unsigned  dst, bdd  cond, bool  acc = true  )

inline

Create an edge from src to dst.

If acc is true, all acceptance sets are set on the edge.

References spot::digraph< State_Data, Edge_Data >::new_edge().

new_edge()

unsigned spot::twa_graph::new_edge ( unsigned  src, unsigned  dst, bdd  cond, acc_cond::mark_t  acc = {}  )

inline

Create a new edge from src to dst.

The edge is labeled with BDD cond and acceptance mark acc. Returns the index of the new edge.

new_state()

unsigned spot::twa_graph::new_state ( )

inline

Create a new state and return its number.

References spot::digraph< State_Data, Edge_Data >::new_state().

new_states()

unsigned spot::twa_graph::new_states ( unsigned  n )

inline

Create n new states; return the number of the first one.

References spot::digraph< State_Data, Edge_Data >::new_states().

new_univ_edge() [1/2]

template<class I >

unsigned spot::twa_graph::new_univ_edge ( unsigned  src, I  begin, I  end, bdd  cond, acc_cond::mark_t  acc = {}  )

inline

Create a universal edge from src to states in [begin, end).

new_univ_edge() [2/2]

unsigned spot::twa_graph::new_univ_edge ( unsigned  src, std::initializer_list< unsigned >  dst, bdd  cond, acc_cond::mark_t  acc = {}  )

inline

Create a universal edge from src to the listed destinations.

num_edges()

unsigned spot::twa_graph::num_edges ( ) const

inline

Returns the number of edges in the automaton.

References spot::digraph< State_Data, Edge_Data >::num_edges().

Referenced by operator==().

num_sets()

unsigned spot::twa::num_sets ( ) const

inlineinherited

Number of acceptance sets used by the automaton.

References spot::acc_cond::num_sets().

Referenced by operator==().

num_states()

unsigned spot::twa_graph::num_states ( ) const

inline

Returns the number of states in the automaton.

References spot::digraph< State_Data, Edge_Data >::num_states().

Referenced by operator==().

operator==()

bool spot::twa_graph::operator== ( const twa_graph &  aut ) const

inline

Structural equality: same states, edges, labels, and acceptance.

References spot::digraph< State_Data, Edge_Data >::dests_vector(), edge_vector(), get_graph(), num_edges(), spot::twa::num_sets(), and num_states().

out() [1/2]

internal::state_out< graph_t > spot::twa_graph::out ( unsigned  src )

inline

Returns a range over outgoing edges of state src.

References spot::digraph< State_Data, Edge_Data >::out().

out() [2/2]

internal::state_out< const graph_t > spot::twa_graph::out ( unsigned  src ) const

inline

Returns a range over outgoing edges of state src (const).

References spot::digraph< State_Data, Edge_Data >::out().

out_iteraser()

internal::killer_edge_iterator< graph_t > spot::twa_graph::out_iteraser ( unsigned  src )

inline

Returns an edge-erasing iterator over outgoing edges of src.

References spot::digraph< State_Data, Edge_Data >::out_iteraser().

project_state()

virtual state * spot::twa::project_state ( const state *  s, const const_twa_ptr &  t  ) const

virtualinherited

Project a state on an automaton.

This converts s, into that corresponding spot::state for t. This is useful when you have the state of a product, and want to restrict this state to a specific automata occurring in the product.

It goes without saying that s and t should be compatible (i.e., s is a state of t).

Returns

0 if the projection fails (s is unrelated to t), or a new state* (the projected state) that must be destroyed by the caller.

Reimplemented in spot::twa_product.

prop_complete() [1/2]

trival spot::twa::prop_complete ( ) const

inlineinherited

Whether the automaton is complete.

An automaton is complete if for each state the union of the labels of its outgoing transitions is always true.

Note that this method may return trival::maybe() when it is unknown whether the automaton is complete or not. If you need a true/false answer, prefer the is_complete() function.

See also

prop_complete()

is_complete()

prop_complete() [2/2]

void spot::twa::prop_complete ( trival  val )

inlineinherited

Set the complete property.

See also

is_complete()

References spot::trival::val().

prop_copy()

void spot::twa::prop_copy ( const const_twa_ptr &  other, prop_set  p  )

inlineinherited

Copy the properties of another automaton.

Copy the property specified with p from other to the current automaton.

There is no default value for p on purpose. This way any time we add a new property we have to update every call to prop_copy().

See also

prop_set

References spot::twa::prop_set::complete, spot::twa::prop_set::deterministic, spot::twa::prop_set::improve_det, spot::twa::prop_set::inherently_weak, spot::twa::prop_set::state_based, and spot::twa::prop_set::stutter_inv.

prop_inherently_weak() [1/2]

trival spot::twa::prop_inherently_weak ( ) const

inlineinherited

Whether the automaton is inherently weak.

An automaton is inherently weak if accepting cycles and rejecting cycles are never mixed in the same strongly connected component.

See also

prop_weak()

prop_terminal()

prop_inherently_weak() [2/2]

void spot::twa::prop_inherently_weak ( trival  val )

inlineinherited

Set the "inherently weak" property.

Setting "inherently weak" to false automatically disables "terminal", "very weak", and "weak".

See also

prop_weak()

prop_terminal()

References spot::trival::val().

prop_keep()

void spot::twa::prop_keep ( prop_set  p )

inlineinherited

Keep only a subset of properties of the current automaton.

All properties part of a group set to false in p are reset to their default value of trival::maybe().

References spot::twa::prop_set::complete, spot::twa::prop_set::deterministic, spot::twa::prop_set::improve_det, spot::twa::prop_set::inherently_weak, spot::twa::prop_set::state_based, and spot::twa::prop_set::stutter_inv.

prop_reset()

void spot::twa::prop_reset ( )

inlineinherited

Reset all automaton properties to trival::maybe().

This is equivalent to prop_keep({}) and causes all automaton properties to be considered unknown.

prop_semi_deterministic() [1/2]

trival spot::twa::prop_semi_deterministic ( ) const

inlineinherited

Whether the automaton is semi-deterministic.

An automaton is semi-deterministic if the sub-automaton reachable from any accepting SCC is universal.

Note that this method may return trival::maybe() when it is unknown whether the automaton is semi-deterministic or not. If you need a true/false answer, prefer the is_semi_deterministic() function.

See also

prop_universal()

is_semi_deterministic()

prop_semi_deterministic() [2/2]

void spot::twa::prop_semi_deterministic ( trival  val )

inlineinherited

Set the semi-deterministic property.

Marking an automaton as "non semi-deterministic" automatically marks it as "non universal".

See also

prop_universal()

References spot::trival::val().

prop_state_acc() [1/2]

trival spot::twa::prop_state_acc ( ) const

inlineinherited

Whether the automaton uses state-based acceptance.

From the point of view of Spot, this means that all transitions leaving a state belong to the same acceptance sets. Then it is equivalent to pretend that the state is in the acceptance set.

prop_state_acc() [2/2]

void spot::twa::prop_state_acc ( trival  val )

inlineinherited

Set the state-based-acceptance property.

If this property is set to true, then all transitions leaving a state must belong to the same acceptance sets.

References spot::trival::val().

prop_stutter_invariant() [1/2]

trival spot::twa::prop_stutter_invariant ( ) const

inlineinherited

Whether the automaton is stutter-invariant.

An automaton is stutter-invariant iff any accepted word remains accepted after removing a finite number of duplicate letters, or after duplicating a finite number of letters.

Note that this method may return trival::maybe() when it is unknown whether the automaton is stutter-invariant or not. If you need a true/false answer, prefer the is_stutter_invariant() function.

See also

is_stutter_invariant

prop_stutter_invariant() [2/2]

void spot::twa::prop_stutter_invariant ( trival  val )

inlineinherited

Set the stutter-invariant property.

References spot::trival::val().

prop_terminal() [1/2]

trival spot::twa::prop_terminal ( ) const

inlineinherited

Whether the automaton is terminal.

An automaton is terminal if it is weak, its accepting strongly connected components are complete, and no accepting edge leads to a non-accepting SCC.

This property ensures that a word can be accepted as soon as one of its prefixes moves through an accepting edge.

See also

prop_weak()

prop_inherently_weak()

prop_terminal() [2/2]

void spot::twa::prop_terminal ( trival  val )

inlineinherited

Set the terminal property.

Marking an automaton as "terminal" automatically marks it as "weak" and "inherently weak".

See also

prop_weak()

prop_inherently_weak()

References spot::trival::val().

prop_unambiguous() [1/2]

trival spot::twa::prop_unambiguous ( ) const

inlineinherited

Whether the automaton is unambiguous.

An automaton is unambiguous if any accepted word is recognized by exactly one accepting path in the automaton. Any word (accepted or not) may be recognized by several rejecting paths in the automaton.

Note that this method may return trival::maybe() when it is unknown whether the automaton is unambiguous or not. If you need a true/false answer, prefer the is_unambiguous() function.

See also

prop_universal()

is_unambiguous()

prop_unambiguous() [2/2]

void spot::twa::prop_unambiguous ( trival  val )

inlineinherited

Set the unambiguous property.

Marking an automaton as "non unambiguous" automatically marks it as "non universal".

See also

prop_deterministic()

References spot::trival::val().

prop_universal() [1/2]

trival spot::twa::prop_universal ( ) const

inlineinherited

Whether the automaton is universal.

An automaton is universal if the conjunction between the labels of two transitions leaving a state is always false.

Note that this method may return trival::maybe() when it is unknown whether the automaton is universal or not. If you need a true/false answer, prefer the is_universal() function.

See also

prop_unambiguous()

is_universal()

prop_universal() [2/2]

void spot::twa::prop_universal ( trival  val )

inlineinherited

Set the universal property.

Setting the "universal" property automatically sets the "unambiguous" and "semi-deterministic" properties.

See also

prop_unambiguous()

prop_semi_deterministic()

References spot::trival::val().

prop_very_weak() [1/2]

trival spot::twa::prop_very_weak ( ) const

inlineinherited

Whether the automaton is very-weak.

An automaton is very-weak if it is weak (inside each strongly connected component, all transitions belong to the same acceptance sets) and each SCC contains only one state.

See also

prop_terminal()

prop_weak()

prop_very_weak() [2/2]

void spot::twa::prop_very_weak ( trival  val )

inlineinherited

Set the very-weak property.

Marking an automaton as "very-weak" automatically marks it as "weak" and "inherently weak".

See also

prop_terminal()

prop_weak()

References spot::trival::val().

prop_weak() [1/2]

trival spot::twa::prop_weak ( ) const

inlineinherited

Whether the automaton is weak.

An automaton is weak if inside each strongly connected component, all transitions belong to the same acceptance sets.

See also

prop_terminal()

prop_inherently_weak()

prop_weak() [2/2]

void spot::twa::prop_weak ( trival  val )

inlineinherited

Set the weak property.

Marking an automaton as "weak" automatically marks it as "inherently weak". Marking an automaton as "not weak" automatically marks it as "not terminal".

See also

prop_terminal()

prop_inherently_weak()

References spot::trival::val().

purge_dead_states()

void spot::twa_graph::purge_dead_states

(

)

Remove all dead states.

Dead states are all the states that cannot be part of an infinite run of the automaton. This includes states without successors, unreachable states, and states that only have dead successors. Transition labeled by bddfalse are also removed.

This function runs in linear time on non-alternating automata, but its current implementation can be quadratic when removing dead states from alternating automata. (In the latter case, a universal edge has to be remove when any of its destination is dead, but this might cause the other destinations to become dead or unreachable themselves.)

See also

purge_unreachable_states

purge_unreachable_states()

void spot::twa_graph::purge_unreachable_states	(	shift_action *	f = nullptr,
		void *	action_data = nullptr
	)

Remove all unreachable states.

Accepts an optional callback f, invoked with a renumbering vector where newst[i]==-1U means state i was deleted.

register_ap() [1/2]

int spot::twa::register_ap ( formula  ap )

inlineinherited

Register an atomic proposition designated by ap.

This is the preferred way to declare that an automaton is using a given atomic proposition.

This adds the atomic proposition to the list of atomic proposition of the automaton, and also registers it to the bdd_dict.

Returns

The BDD variable number assigned for this atomic proposition.

References spot::ap.

register_ap() [2/2]

int spot::twa::register_ap ( std::string  ap )

inlineinherited

Register an atomic proposition designated by ap.

This is the preferred way to declare that an automaton is using a given atomic proposition.

This adds the atomic proposition to the list of atomic proposition of the automaton, and also registers it to the bdd_dict.

Returns

The BDD variable number assigned for this atomic proposition.

References spot::ap.

register_aps_from_dict()

void spot::twa::register_aps_from_dict ( )

inlineinherited

Register all atomic propositions that have already been registered by the bdd_dict for this automaton.

This method may only be called on an automaton with an empty list of AP. It will fetch all atomic propositions that have been set in the bdd_dict for this particular automaton.

The typical use-case for this function is when the labels of an automaton are created by functions such as formula_to_bdd(). This is for instance done in the parser for never claims or LBTT.

release_formula_namer()

void spot::twa_graph::release_formula_namer	(	namer< formula > *	namer,
		bool	keep_names
	)

Release a formula namer.

If keep_names is true, state names are preserved as a named property of the automaton.

release_iter()

void spot::twa::release_iter ( twa_succ_iterator *  i ) const

inlineinherited

Release an iterator after usage.

This iterator can then be reused by succ_iter() to avoid memory allocation.

release_named_properties()

void spot::twa::release_named_properties ( )

inlineinherited

Destroy all named properties.

This is used by the automaton destructor, but it could be used by any algorithm that wants to get rid of all named properties.

remove_unused_ap()

void spot::twa_graph::remove_unused_ap

(

)

Remove unused atomic propositions.

Remove, from the list of atomic propositions registered by the automaton, those that are not actually used by its labels.

rename_states_()

void spot::twa_graph::rename_states_

(

const std::vector< unsigned > &

newst

)

Rename all states.

This semi-internal function is a wrapper around digraph::rename_states_() that additionally updates init_state and all named properties that depend on state numbers.

set_acceptance() [1/2]

void spot::twa::set_acceptance ( const acc_cond &  c )

inlineinherited

Set the acceptance condition of the automaton.

Parameters

c	another acceptance condition

set_acceptance() [2/2]

void spot::twa::set_acceptance ( unsigned  num, const acc_cond::acc_code &  c  )

inlineinherited

Set the acceptance condition of the automaton.

Parameters

num	the number of acceptance sets used
c	the acceptance formula

set_buchi()

acc_cond::mark_t spot::twa::set_buchi ( )

inlineinherited

Set Büchi acceptance.

This declares a single acceptance set, and Inf(0) acceptance. The returned mark {0} can be used to tag accepting transitions.

Note that this does not mark the automaton as using state-based acceptance. If you want to create a Büchi automaton with state-based acceptance, call

prop_state_acc(true)

in addition.

See also

prop_state_acc

set_co_buchi()

acc_cond::mark_t spot::twa::set_co_buchi ( )

inlineinherited

Set co-Büchi acceptance.

This declares a single acceptance set, and Fin(0) acceptance. The returned mark {0} can be used to tag non-accepting transitions.

Note that this does not mark the automaton as using state-based acceptance. If you want to create a co-Büchi automaton with state-based acceptance, call

prop_state_acc(true)

in addition.

See also

prop_state_acc

set_generalized_buchi()

void spot::twa::set_generalized_buchi ( unsigned  num )

inlineinherited

Set generalized Büchi acceptance.

Parameters

num	the number of acceptance sets to use

The acceptance formula of the form

Inf(0)&Inf(1)&...&Inf(num-1)

is generated.

In the case where num is null, the state-acceptance property is automatically turned on.

set_generalized_co_buchi()

void spot::twa::set_generalized_co_buchi ( unsigned  num )

inlineinherited

Set generalized co-Büchi acceptance.

Parameters

num	the number of acceptance sets to use

The acceptance formula of the form

Fin(0)&Fin(1)&...&Fin(num-1)

is generated.

In the case where num is null, the state-acceptance property is automatically turned on.

set_init_state()

void spot::twa_graph::set_init_state ( state_num  s )

inline

Set the initial state to state number s.

References spot::digraph< State_Data, Edge_Data >::dests_vector().

set_named_prop() [1/3]

void spot::twa::set_named_prop ( std::string  s, std::nullptr_t    )

inherited

Erase a named property.

Arbitrary objects can be attached to automata. Those are called named properties. They are used for instance to name all the states of an automaton.

This function removes the property s if it exists.

See https://spot.lrde.epita.fr/concepts.html#named-properties for a list of named properties used by Spot.

set_named_prop() [2/3]

template<typename T >

void spot::twa::set_named_prop ( std::string  s, T *  val  )

inlineinherited

Declare a named property.

Arbitrary objects can be attached to automata. Those are called named properties. They are used for instance to name all the states of an automaton.

This function attaches the object val to the current automaton, under the name s and destroys any previous property with the same name.

When the automaton is destroyed, the attached object will be destroyed with delete.

See https://spot.lrde.epita.fr/concepts.html#named-properties for a list of named properties used by Spot.

set_named_prop() [3/3]

void spot::twa::set_named_prop ( std::string  s, void *  val, std::function< void(void *)>  destructor  )

inherited

Declare a named property.

Arbitrary objects can be attached to automata. Those are called named properties. They are used for instance to name all the states of an automaton.

This function attaches the object val to the current automaton, under the name s and destroys any previous property with the same name.

When the automaton is destroyed, the destructor function will be called to destroy the attached object.

See https://spot.lrde.epita.fr/concepts.html#named-properties for a list of named properties used by Spot.

set_univ_init_state() [1/2]

void spot::twa_graph::set_univ_init_state ( const std::initializer_list< state_num > &  il )

inline

Set a universal initial state from an initializer list.

set_univ_init_state() [2/2]

template<class I >

void spot::twa_graph::set_univ_init_state ( I  dst_begin, I  dst_end  )

inline

Set a universal initial state from a range of destination states.

References spot::digraph< State_Data, Edge_Data >::new_univ_dests().

state_acc_sets()

acc_cond::mark_t spot::twa_graph::state_acc_sets ( unsigned  s ) const

inline

Return the marks associated to a state if the acceptance is state-based.

References spot::digraph< State_Data, Edge_Data >::out().

state_from_number()

const twa_graph_state * spot::twa_graph::state_from_number ( state_num  n ) const

inline

Returns the state pointer for state number n.

References spot::digraph< State_Data, Edge_Data >::state_data().

state_is_accepting() [1/2]

bool spot::twa_graph::state_is_accepting ( const state *  s ) const

inline

Tell if a state is accepting.

This makes only sense for automata using state-based acceptance, and a simple acceptance condition like Büchi or co-Büchi.

state_is_accepting() [2/2]

bool spot::twa_graph::state_is_accepting ( unsigned  s ) const

inline

Tell if a state is accepting.

This makes only sense for automata using state-based acceptance, and a simple acceptance condition like Büchi or co-Büchi.

References spot::digraph< State_Data, Edge_Data >::out().

state_number()

state_num spot::twa_graph::state_number ( const state *  st ) const

inline

Returns the state number corresponding to state pointer st.

References spot::digraph< State_Data, Edge_Data >::state_storage().

states() [1/2]

auto spot::twa_graph::states

(

)

const

Returns a range over all states (const).

states() [2/2]

auto spot::twa_graph::states

(

)

Returns a range over all states.

succ()

internal::twa_succ_iterable spot::twa::succ ( const state *  s ) const

inlineinherited

Build an iterable over the successors of s.

This is meant to be used as

for (auto i: aut->succ(s))
  {
    // use i->cond(), i->acc(), i->dst()
  }

and the above loop is in fact syntactic sugar for

twa_succ_iterator* i = aut->succ_iter(s);
if (i->first())
  do
    {
      // use i->cond(), i->acc(), i->dst()
    }
  while (i->next());
aut->release_iter(i);

succ_iter()

virtual twa_succ_iterator * spot::twa_graph::succ_iter ( const state *  local_state ) const

inlineoverridevirtual

Get an iterator over the successors of local_state.

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

See also

succ()

Implements spot::twa.

References spot::digraph< State_Data, Edge_Data >::is_valid_edge().

univ_dests() [1/2]

internal::const_universal_dests spot::twa_graph::univ_dests ( const edge_storage_t &  e ) const

inlinenoexcept

Returns the universal destinations of edge e.

References spot::digraph< State_Data, Edge_Data >::univ_dests().

univ_dests() [2/2]

internal::const_universal_dests spot::twa_graph::univ_dests ( unsigned  d ) const

inlinenoexcept

Returns the universal destinations of dest-index d.

References spot::digraph< State_Data, Edge_Data >::univ_dests().

unregister_ap()

void spot::twa::unregister_ap ( int  num )

inherited

Unregister an atomic proposition.

Parameters

num	the BDD variable number returned by register_ap().

Member Data Documentation

dict_

bdd_dict_ptr spot::twa::dict_

protectedinherited

BDD dictionary used by the automaton.

g_

graph_t spot::twa_graph::g_

protected

The underlying graph.

init_number_

unsigned spot::twa_graph::init_number_

mutableprotected

Number of the initial state.

is

bprop spot::twa::is

inherited

Named access to individual property flags.

iter_cache_

twa_succ_iterator* spot::twa::iter_cache_

mutableprotectedinherited

Any iterator returned via release_iter.

named_prop_

std::unordered_map<std::string, std::pair<void*, std::function<void(void*)> > > spot::twa::named_prop_

protectedinherited

Storage for named properties.

Maps property names to (pointer, destructor) pairs.

props

unsigned spot::twa::props

inherited

All property flags packed as a bitmask.

---

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

• spot/twa/twagraph.hh