spot::twa Class Reference

A Transition-based ω-Automaton. More...

#include <spot/twa/twa.hh>

Inheritance diagram for spot::twa:

Collaboration diagram for spot::twa:

Public Member Functions
virtual const state *	get_init_state () const =0
	Get the initial state of the automaton. More...
virtual twa_succ_iterator *	succ_iter (const state *local_state) const =0
	Get an iterator over the successors of local_state. More...
internal::twa_succ_iterable	succ (const state *s) const
	Build an iterable over the successors of s. More...
void	release_iter (twa_succ_iterator *i) const
	Release an iterator after usage. More...
bdd_dict_ptr	get_dict () const
	Get the dictionary associated to the automaton. More...
void	unregister_ap (int num)
	Unregister an atomic proposition. More...
void	register_aps_from_dict ()
	Register all atomic propositions that have already been registered by the bdd_dict for this automaton. More...
const std::vector< formula > &	ap () const
	The vector of atomic propositions registered by this automaton. More...
bdd	ap_vars () const
	The set of atomic propositions as a conjunction. More...
virtual std::string	format_state (const state *s) const =0
	Format the state as a string for printing. More...
virtual state *	project_state (const state *s, const const_twa_ptr &t) const
	Project a state on an automaton. More...
virtual bool	is_empty () const
	Check whether the language of the automaton is empty. More...
virtual twa_run_ptr	accepting_run () const
	Return an accepting run if one exists. More...
virtual twa_word_ptr	accepting_word () const
	Return an accepting word if one exists. More...
virtual bool	intersects (const_twa_ptr other) const
	Check whether the language of this automaton intersects that of the other automaton. More...
virtual bool	intersects (const_twa_word_ptr w) const
	Check if this automaton _word intersects a word. More...
virtual twa_run_ptr	intersecting_run (const_twa_ptr other) const
	Return an accepting run recognizing a word accepted by two automata. More...
	SPOT_DEPRECATED ("replace a->intersecting_run(b, true) " "by b->intersecting_run(a).") twa_run_ptr intersecting_run(const_twa_ptr other
else return this	intersecting_run (other)
virtual twa_word_ptr	intersecting_word (const_twa_ptr other) const
	Return a word accepted by two automata. More...
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. More...
virtual twa_word_ptr	exclusive_word (const_twa_ptr other) const
	Return a word accepted by exactly one of the two automata. More...
unsigned	num_sets () const
	Number of acceptance sets used by the automaton. More...
const acc_cond::acc_code &	get_acceptance () const
	Acceptance formula used by the automaton. More...
void	set_acceptance (unsigned num, const acc_cond::acc_code &c)
	Set the acceptance condition of the automaton. More...
void	set_acceptance (const acc_cond &c)
	Set the acceptance condition of the automaton. More...
void	copy_acceptance_of (const const_twa_ptr &a)
	Copy the acceptance condition of another TωA. More...
void	copy_ap_of (const const_twa_ptr &a)
	Copy the atomic propositions of another TωA. More...
void	copy_named_properties_of (const const_twa_ptr &a)
	Copy all the named properties of a into this automaton. More...
void	set_generalized_buchi (unsigned num)
	Set generalized Büchi acceptance. More...
void	set_generalized_co_buchi (unsigned num)
	Set generalized co-Büchi acceptance. More...
acc_cond::mark_t	set_buchi ()
	Set Büchi acceptance. More...
acc_cond::mark_t	set_co_buchi ()
	Set co-Büchi acceptance. More...
void	set_named_prop (std::string s, void *val, std::function< void(void *)> destructor)
	Declare a named property. More...
template<typename T >
void	set_named_prop (std::string s, T *val)
	Declare a named property. More...
void	set_named_prop (std::string s, std::nullptr_t)
	Erase a named property. More...
template<typename T >
T *	get_named_prop (std::string s) const
	Retrieve a named property. More...
template<typename T >
T *	get_or_set_named_prop (std::string s)
	Create or retrieve a named property. More...
void	release_named_properties ()
	Destroy all named properties. More...
trival	prop_state_acc () const
	Whether the automaton uses state-based acceptance. More...
void	prop_state_acc (trival val)
	Set the state-based-acceptance property. More...
trival	is_sba () const
	Whether this is a state-based Büchi automaton. More...
trival	prop_inherently_weak () const
	Whether the automaton is inherently weak. More...
void	prop_inherently_weak (trival val)
	Set the "inherently weak" property. More...
trival	prop_terminal () const
	Whether the automaton is terminal. More...
void	prop_terminal (trival val)
	Set the terminal property. More...
trival	prop_weak () const
	Whether the automaton is weak. More...
void	prop_weak (trival val)
	Set the weak property. More...
trival	prop_very_weak () const
	Whether the automaton is very-weak. More...
void	prop_very_weak (trival val)
	Set the very-weak property. More...
trival	prop_complete () const
	Whether the automaton is complete. More...
void	prop_complete (trival val)
	Set the complete property. More...
trival	prop_universal () const
	Whether the automaton is universal. More...
void	prop_universal (trival val)
	Set the universal property. More...
void	prop_deterministic (trival val)
trival	prop_deterministic () const
trival	prop_unambiguous () const
	Whether the automaton is unambiguous. More...
void	prop_unambiguous (trival val)
	Set the unambiguous property. More...
trival	prop_semi_deterministic () const
	Whether the automaton is semi-deterministic. More...
void	prop_semi_deterministic (trival val)
	Set the semi-deterministic property. More...
trival	prop_stutter_invariant () const
	Whether the automaton is stutter-invariant. More...
void	prop_stutter_invariant (trival val)
	Set the stutter-invariant property. More...
int	register_ap (formula ap)
	Register an atomic proposition designated by ap. More...
int	register_ap (std::string ap)
	Register an atomic proposition designated by ap. More...
const acc_cond &	acc () const
	The acceptance condition of the automaton. More...
acc_cond &	acc ()
	The acceptance condition of the automaton. More...

Static Public Member Functions
static prop_set	all ()
	A structure for selecting a set of automaton properties to copy. More...

Public Attributes
bool from_other	const
unsigned	props
bprop	is

Protected Member Functions
	twa (const bdd_dict_ptr &d)
void *	get_named_prop_ (std::string s) const

Protected Attributes
twa_succ_iterator *	iter_cache_
	Any iterator returned via release_iter. More...
bdd_dict_ptr	dict_
	BDD dictionary used by the automaton. More...
std::unordered_map< std::string, std::pair< void *, std::function< void(void *)> > >	named_prop_

Detailed Description

A Transition-based ω-Automaton.

The acronym TωA stands for Transition-based ω-automaton. We may write it as TwA or twa, but never as TWA as the w is just a non-utf8 replacement for ω that should not be capitalized.

TωAs are transition-based automata, meaning that not-only do they have labels on edges, but they also have an acceptance condition defined in terms of sets of transitions. The acceptance condition can be anything supported by the HOA format (http://adl.github.io/hoaf/). The only restriction w.r.t. the format is that this class does not support alternating automata.

Previous versions of Spot supported a type of automata called TGBA, which are TωA in which the acceptance condition is a set of sets of transitions that must be visited infinitely often.

In this version, TGBAs are now represented by TωAs for which

aut->acc().is_generalized_buchi()

returns true.

Browsing a TωA is usually achieved using two methods: get_init_state(), and succ(). The former returns the initial state while the latter allows iterating over the outgoing edges of any given state. A TωA is always assumed to have at least one state, the initial one.

Note that although this is a transition-based automaton, we never represent edges in the API. Information about edges can be obtained by querying the iterator over the successors of a state.

The interface presented here is what we call the on-the-fly interface of automata, because the TωA class can be subclassed to implement an object that computes its successors on-the-fly. The down-side is that all these methods are virtual, so you pay the cost of virtual calls when iterating over automata constructed on-the-fly. Also the interface assumes that each successor state is a new object whose memory management is the responsibility of the caller, who should then call state::destroy() to release it.

If you want to work with a TωA that is explicitly stored as a graph in memory, use the spot::twa_graph subclass instead. A twa_graph object can be used as a spot::twa (using the on-the-fly interface, even though nothing needs to be constructed), but it also offers a faster interface that does not use virtual methods.

Member Function Documentation

acc() [1/2]

acc_cond & spot::twa::acc ( )

inline

The acceptance condition of the automaton.

acc() [2/2]

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

inline

The acceptance condition of the automaton.

accepting_run()

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

virtual

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

virtual

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.

all()

static prop_set spot::twa::all ( )

inlinestatic

A structure for selecting a set of automaton properties to copy.

When an algorithm copies an automaton before making some modification on that automaton, it should use a prop_set structure to indicate which properties should be copied from the original automaton.

This structure does not list all supported properties, because properties are copied by groups of related properties. For instance if an algorithm breaks the "inherent_weak" properties, it usually also breaks the "weak" and "terminal" properties.

Set the flags to true to copy the value of the original property, and to false to ignore the original property (leaving the property of the new automaton to its default value, which is trival::maybe()).

This can be used for instance as:

aut->prop_copy(other_aut, {true, false, false, false, false, true});

This would copy the "state-based acceptance" and "stutter invariant" properties from other_aut to code.

There are two flags for the determinism. If

    deterministic is set, the universal, semi-deterministic,
    and unambiguous properties are copied as-is.  If deterministic
    is unset but improve_det is set, then those properties are
    only copied if they are positive.
   
    The reason there is no default value for these flags is that
    whenever we add a new property that does not fall into any of
    these groups, we will be forced to review all algorithms to
    decide if the property should be preserved or not.
   
    \see make_twa_graph_ptr
    \see prop_copy
struct prop_set
{
  bool state_based;     
  bool inherently_weak; 
  bool deterministic;   
  bool improve_det;     
  bool complete;        
  bool stutter_inv;     
 
  prop_set()
  : state_based(false),
    inherently_weak(false),
    deterministic(false),
    improve_det(false),
    complete(false),
    stutter_inv(false)
  {
  }
 
  prop_set(bool state_based,
           bool inherently_weak,
           bool deterministic,
           bool improve_det,
           bool complete,
           bool stutter_inv)
  : state_based(state_based),
    inherently_weak(inherently_weak),
    deterministic(deterministic),
    improve_det(improve_det),
    complete(complete),
    stutter_inv(stutter_inv)
  {
  }
 
 
  // The "complete" argument was added in Spot 2.4
 
  prop_set(bool state_based,
           bool inherently_weak,
           bool deterministic,
           bool improve_det,
           bool stutter_inv)
  : state_based(state_based),
    inherently_weak(inherently_weak),
    deterministic(deterministic),
    improve_det(improve_det),
    complete(false),
    stutter_inv(stutter_inv)
  {
  }
 
 
      \brief An all-true \c prop_set
     
      Use that only in algorithms that copy an automaton without
      performing any modification.
     
      If an algorithm X does modifications, but preserves all the
      properties currently implemented, use an explicit
     
      \code
         {true, true, true, true, true, true}

instead of calling all(). This way, the day a new property is added, we will still be forced to review algorithm X, in case that new property is not preserved.

ap()

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

inline

The vector of atomic propositions registered by this automaton.

ap_vars()

bdd spot::twa::ap_vars ( ) const

inline

The set of atomic propositions as a conjunction.

copy_acceptance_of()

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

inline

Copy the acceptance condition of another TωA.

copy_ap_of()

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

inline

Copy the atomic propositions of another TωA.

copy_named_properties_of()

void spot::twa::copy_named_properties_of

(

const const_twa_ptr &

a

)

Copy all the named properties of a into this automaton.

exclusive_run()

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

virtual

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

virtual

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()

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

pure virtual

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.

Implemented in spot::tgta_explicit, spot::taa_tgba_labelled< label >, spot::taa_tgba_labelled< formula >, spot::taa_tgba_labelled< std::string >, spot::kripke_graph, spot::twa_graph, and spot::twa_product.

get_acceptance()

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

inline

Acceptance formula used by the automaton.

References spot::acc_cond::get_acceptance().

get_dict()

bdd_dict_ptr spot::twa::get_dict ( ) const

inline

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_init_state()

virtual const state * spot::twa::get_init_state ( ) const

pure virtual

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.

Implemented in spot::kripke_graph, spot::tgta_explicit, spot::tgta_product, spot::twa_graph, spot::twa_product, spot::twa_product_init, and spot::taa_tgba.

get_named_prop()

template<typename T >

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

inline

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_or_set_named_prop()

template<typename T >

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

inline

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

virtual

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

virtual

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

virtual

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

virtual

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_empty()

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

virtual

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_sba()

trival spot::twa::is_sba ( ) const

inline

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.

num_sets()

unsigned spot::twa::num_sets ( ) const

inline

Number of acceptance sets used by the automaton.

References spot::acc_cond::num_sets().

project_state()

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

virtual

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

inline

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 )

inline

Set the complete property.

See also

is_complete()

prop_inherently_weak() [1/2]

trival spot::twa::prop_inherently_weak ( ) const

inline

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 )

inline

Set the "inherently weak" property.

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

See also

prop_weak()

prop_terminal()

prop_semi_deterministic() [1/2]

trival spot::twa::prop_semi_deterministic ( ) const

inline

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 )

inline

Set the semi-deterministic property.

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

See also

prop_universal()

prop_state_acc() [1/2]

trival spot::twa::prop_state_acc ( ) const

inline

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 )

inline

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.

prop_stutter_invariant() [1/2]

trival spot::twa::prop_stutter_invariant ( ) const

inline

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 )

inline

Set the stutter-invariant property.

prop_terminal() [1/2]

trival spot::twa::prop_terminal ( ) const

inline

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 )

inline

Set the terminal property.

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

See also

prop_weak()

prop_inherently_weak()

prop_unambiguous() [1/2]

trival spot::twa::prop_unambiguous ( ) const

inline

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 )

inline

Set the unambiguous property.

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

See also

prop_deterministic()

prop_universal() [1/2]

trival spot::twa::prop_universal ( ) const

inline

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 )

inline

Set the universal property.

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

See also

prop_unambiguous()

prop_semi_deterministic()

prop_very_weak() [1/2]

trival spot::twa::prop_very_weak ( ) const

inline

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 )

inline

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()

prop_weak() [1/2]

trival spot::twa::prop_weak ( ) const

inline

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 )

inline

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()

register_ap() [1/2]

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

inline

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 )

inline

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, and spot::formula::ap().

register_aps_from_dict()

void spot::twa::register_aps_from_dict ( )

inline

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_iter()

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

inline

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 ( )

inline

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.

set_acceptance() [1/2]

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

inline

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  )

inline

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 ( )

inline

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

References spot::acc_cond::acc_code::buchi().

set_co_buchi()

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

inline

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

References spot::acc_cond::acc_code::cobuchi().

set_generalized_buchi()

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

inline

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.

References spot::acc_cond::acc_code::generalized_buchi().

set_generalized_co_buchi()

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

inline

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.

References spot::acc_cond::acc_code::generalized_co_buchi().

set_named_prop() [1/3]

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

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  )

inline

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
	)

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.

succ()

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

inline

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::succ_iter ( const state *  local_state ) const

pure virtual

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()

Implemented in spot::tgta_explicit, spot::kripke_graph, spot::taa_tgba, spot::tgta_product, spot::twa_graph, and spot::twa_product.

unregister_ap()

void spot::twa::unregister_ap

(

int

num

)

Unregister an atomic proposition.

Parameters

num	the BDD variable number returned by register_ap().

Member Data Documentation

const

bool from_other spot::twa::const

Initial value:

{
      if (from_other)
        return other->intersecting_run(shared_from_this())

dict_

bdd_dict_ptr spot::twa::dict_

protected

BDD dictionary used by the automaton.

iter_cache_

twa_succ_iterator* spot::twa::iter_cache_

mutableprotected

Any iterator returned via release_iter.

---

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

• spot/twa/twa.hh