spot
2.11.3

Graphbased representation of a TωA. More...
#include <spot/twa/twagraph.hh>
Public Types  
typedef digraph< twa_graph_state, twa_graph_edge_data >  graph_t 
typedef spot::internal::edge_storage< unsigned, unsigned, unsigned, internal::boxed_label< twa_graph_edge_data, false > >  edge_storage_t 
typedef unsigned  state_num 
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 > 
typedef void(*  shift_action) (const std::vector< unsigned > &newst, void *action_data) 
Remove all unreachable states. More...  
Public Member Functions  
void  apply_permutation (std::vector< unsigned > permut) 
twa_graph (const bdd_dict_ptr &dict)  
twa_graph (const const_twa_graph_ptr &other, prop_set 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 () 
namer< formula > *  create_formula_namer () 
void  release_formula_namer (namer< formula > *namer, bool keep_names) 
graph_t &  get_graph () 
const graph_t &  get_graph () const 
unsigned  num_states () const 
unsigned  num_edges () const 
void  set_init_state (state_num s) 
template<class I >  
void  set_univ_init_state (I dst_begin, I dst_end) 
void  set_univ_init_state (const std::initializer_list< state_num > &il) 
state_num  get_init_state_number () const 
virtual const twa_graph_state *  get_init_state () const override 
Get the initial state of the automaton. More...  
virtual twa_succ_iterator *  succ_iter (const state *st) const override 
Get an iterator over the successors of local_state. More...  
state_num  state_number (const state *st) const 
const twa_graph_state *  state_from_number (state_num n) const 
std::string  format_state (unsigned n) const 
virtual std::string  format_state (const state *st) const override 
Format the state as a string for printing. More...  
unsigned  edge_number (const twa_succ_iterator *it) const 
unsigned  edge_number (const edge_storage_t &e) const 
twa_graph_edge_data &  edge_data (const twa_succ_iterator *it) 
twa_graph_edge_data &  edge_data (unsigned t) 
const twa_graph_edge_data &  edge_data (const twa_succ_iterator *it) const 
const twa_graph_edge_data &  edge_data (unsigned t) const 
edge_storage_t &  edge_storage (const twa_succ_iterator *it) 
edge_storage_t &  edge_storage (unsigned t) 
const edge_storage_t  edge_storage (const twa_succ_iterator *it) const 
const edge_storage_t  edge_storage (unsigned t) const 
unsigned  new_state () 
unsigned  new_states (unsigned n) 
unsigned  new_edge (unsigned src, unsigned dst, bdd cond, acc_cond::mark_t acc={}) 
unsigned  new_acc_edge (unsigned src, unsigned dst, bdd cond, bool acc=true) 
template<class I >  
unsigned  new_univ_edge (unsigned src, I begin, I end, bdd cond, acc_cond::mark_t acc={}) 
unsigned  new_univ_edge (unsigned src, std::initializer_list< unsigned > dst, bdd cond, acc_cond::mark_t acc={}) 
internal::state_out< const graph_t >  out (unsigned src) const 
internal::state_out< graph_t >  out (unsigned src) 
internal::killer_edge_iterator< graph_t >  out_iteraser (unsigned src) 
internal::const_universal_dests  univ_dests (unsigned d) const noexcept 
internal::const_universal_dests  univ_dests (const edge_storage_t &e) const noexcept 
bool  is_existential () const 
Whether the automaton uses only existential branching. More...  
auto  states () const SPOT_RETURN(g_.states()) 
auto  states () SPOT_RETURN(g_.states()) 
internal::all_trans< const graph_t >  edges () const noexcept 
internal::all_trans< graph_t >  edges () noexcept 
auto  edge_vector () const SPOT_RETURN(g_.edge_vector()) 
auto  edge_vector () SPOT_RETURN(g_.edge_vector()) 
bool  is_dead_edge (unsigned t) const 
bool  is_dead_edge (const graph_t::edge_storage_t &t) const 
void  merge_edges () 
Merge edges that can be merged. More...  
void  merge_univ_dests () 
Merge common universal destinations. More...  
unsigned  merge_states (parallel_policy ppolicy=parallel_policy()) 
Merge states that can be merged. More...  
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. More...  
void  purge_dead_states () 
Remove all dead states. More...  
void  purge_unreachable_states (shift_action *f=nullptr, void *action_data=nullptr) 
void  remove_unused_ap () 
Remove unused atomic propositions. More...  
void  copy_state_names_from (const const_twa_graph_ptr &other) 
Define the state names of this automaton using the names from other. More...  
acc_cond::mark_t  state_acc_sets (unsigned s) const 
Return the marks associated to a state if the acceptance is statebased. More...  
bool  operator== (const twa_graph &aut) const 
void  kill_state (unsigned state) 
Make a state dead. More...  
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. 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 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 twa_run_ptr  intersecting_run (const_twa_ptr other) const 
Return an accepting run recognizing a word accepted by two automata. More...  
else return this  intersecting_run (other) 
SPOT_DEPRECATED ("replace a>intersecting_run(b, true) " "by b>intersecting_run(a).") twa_run_ptr intersecting_run(const_twa_ptr 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 coBüchi acceptance. More...  
acc_cond::mark_t  set_buchi () 
Set Büchi acceptance. More...  
acc_cond::mark_t  set_co_buchi () 
Set coBü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 statebased acceptance. More...  
void  prop_state_acc (trival val) 
Set the statebasedacceptance property. More...  
trival  is_sba () const 
Whether this is a statebased 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 veryweak. More...  
void  prop_very_weak (trival val) 
Set the veryweak 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 semideterministic. More...  
void  prop_semi_deterministic (trival val) 
Set the semideterministic property. More...  
trival  prop_stutter_invariant () const 
Whether the automaton is stutterinvariant. More...  
void  prop_stutter_invariant (trival val) 
Set the stutterinvariant property. More...  
bool  state_is_accepting (unsigned s) const 
Tell if a state is accepting. More...  
bool  state_is_accepting (const state *s) const 
Tell if a state is accepting. More...  
void  defrag_states (std::vector< unsigned > &newst, unsigned used_states) 
Renumber all states, and drop some. More...  
void  defrag_states (std::vector< unsigned > &&newst, unsigned used_states) 
Renumber all states, and drop some. 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 constexpr bool  is_univ_dest (const edge_storage_t &e) 
static constexpr bool  is_univ_dest (unsigned s) 
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  
void *  get_named_prop_ (std::string s) const 
Protected Attributes  
graph_t  g_ 
unsigned  init_number_ 
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_ 
Graphbased representation of a TωA.
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].

inlineinherited 
The acceptance condition of the automaton.

inlineinherited 
The acceptance condition of the automaton.

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 Finacceptance, this computation is not performed onthefly. Any onthefly automaton would be automatically copied into a twa_graph_ptr first.

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 Finacceptance, this computation is not performed onthefly. Any onthefly automaton would be automatically copied into a twa_graph_ptr first.

inlinestaticinherited 
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:
This would copy the "statebased acceptance" and "stutter invariant" properties from other_aut
to code
.
There are two flags for the determinism. If
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.

inlineinherited 
The vector of atomic propositions registered by this automaton.

inlineinherited 
The set of atomic propositions as a conjunction.

inlineinherited 
Copy the acceptance condition of another TωA.

inlineinherited 
Copy the atomic propositions of another TωA.

inherited 
Copy all the named properties of a into this automaton.
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 "originalstates" named property is set, it is used to map the state numbers, otherwise an identity mapping is assumed.

inline 
Renumber all states, and drop some.
This semiinternal 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.
newst  A vector indicating how each state should be renumbered. Use 1U to mark an unreachable state for removal. Ignoring the occurrences of 1U, the renumbering is expected to satisfy newst[i] ≤ i for all i. 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. 
void spot::twa_graph::defrag_states  (  std::vector< unsigned > &  newst, 
unsigned  used_states  
) 
Renumber all states, and drop some.
This semiinternal 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.
newst  A vector indicating how each state should be renumbered. Use 1U to mark an unreachable state for removal. Ignoring the occurrences of 1U, the renumbering is expected to satisfy newst[i] ≤ i for all i. 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. 
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.

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.

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.

inlineoverridevirtual 
Format the state as a string for printing.
Formating is the responsability 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.

inlineinherited 
Acceptance formula used by the automaton.
References spot::acc_cond::get_acceptance().

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.

inlineoverridevirtual 
Get the initial state of the automaton.
The state has been allocated with new
. It is the responsability of the caller to destroy
it when no longer needed.
Implements spot::twa.

inlineinherited 
Retrieve a named property.
Because named property can be object of any type, retrieving the object requires knowing its type.
s  the name of the object to retrieve 
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#namedproperties for a list of named properties used by Spot.

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#namedproperties for a list of named properties used by Spot.

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 onthefly, unless some of the operands use Finacceptance: in this case an explicit product is performed.

virtualinherited 
Return a word accepted by two automata.
Return nullptr if no accepting word were found.

virtualinherited 
Check whether the language of this automaton intersects that of the other automaton.
An emptiness check is performed on a product computed onthefly, unless some of the operands use Finacceptance: in this case an explicit product is performed.

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 Finacceptance, the emptiness check is not performed onthefly. Any onthefly automaton would be automatically copied into a twa_graph_ptr first.

inline 
Whether the automaton uses only existential branching.
References spot::digraph< State_Data, Edge_Data >::is_existential().

inlineinherited 
Whether this is a statebased Büchi automaton.
An SBA has a Büchi acceptance, and should have its statebased acceptance property set.
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.
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 Finless 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.
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 selfloops 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 selfloop equivalences in nondeterministic 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.
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.
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 differd from merge_states(). It is more costly, but is more precise, in the sense that more states are merged. 
void spot::twa_graph::merge_univ_dests  (  ) 
Merge common universal destinations.
This is already called by merge_edges().

inlineinherited 
Number of acceptance sets used by the automaton.
References spot::acc_cond::num_sets().

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 occuring in the product.
It goes without saying that s and t should be compatible (i.e., s is a state of t).
state*
(the projected state) that must be destroyed by the caller. Reimplemented in spot::twa_product.

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.

inlineinherited 
Set the complete property.

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.

inlineinherited 
Set the "inherently weak" property.
Setting "inherently weak" to false automatically disables "terminal", "very weak", and "weak".

inlineinherited 
Whether the automaton is semideterministic.
An automaton is semideterministic if the subautomaton reachable from any accepting SCC is universal.
Note that this method may return trival::maybe() when it is unknown whether the automaton is semideterministic or not. If you need a true/false answer, prefer the is_semi_deterministic() function.

inlineinherited 
Set the semideterministic property.
Marking an automaton as "non semideterministic" automatically marks it as "non universal".

inlineinherited 
Whether the automaton uses statebased 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.

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

inlineinherited 
Whether the automaton is stutterinvariant.
An automaton is stutterinvariant 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 stutterinvariant or not. If you need a true/false answer, prefer the is_stutter_invariant() function.

inlineinherited 
Set the stutterinvariant property.

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 nonaccepting SCC.
This property ensures that a word can be accepted as soon as one of its prefixes moves through an accepting edge.

inlineinherited 
Set the terminal property.
Marking an automaton as "terminal" automatically marks it as "weak" and "inherently weak".

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.

inlineinherited 
Set the unambiguous property.
Marking an automaton as "non unambiguous" automatically marks it as "non universal".

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.

inlineinherited 
Set the universal property.
Setting the "universal" property automatically sets the "unambiguous" and "semideterministic" properties.

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

inlineinherited 
Set the veryweak property.
Marking an automaton as "veryweak" automatically marks it as "weak" and "inherently weak".

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

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".
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 nonalternating 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.)

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

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 usecase 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.

inlineinherited 
Release an iterator after usage.
This iterator can then be reused by succ_iter() to avoid memory allocation.

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.
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.

inlineinherited 
Set the acceptance condition of the automaton.
c  another acceptance condition 

inlineinherited 
Set the acceptance condition of the automaton.
num  the number of acceptance sets used 
c  the acceptance formula 

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 statebased acceptance. If you want to create a Büchi automaton with statebased acceptance, call
in addition.
References spot::acc_cond::acc_code::buchi().

inlineinherited 
Set coBüchi acceptance.
This declares a single acceptance set, and Fin(0)
acceptance. The returned mark {0}
can be used to tag nonaccepting transitions.
Note that this does not mark the automaton as using statebased acceptance. If you want to create a coBüchi automaton with statebased acceptance, call
in addition.
References spot::acc_cond::acc_code::cobuchi().

inlineinherited 
Set generalized Büchi acceptance.
num  the number of acceptance sets to use 
The acceptance formula of the form
is generated.
In the case where num is null, the stateacceptance property is automatically turned on.
References spot::acc_cond::acc_code::generalized_buchi().

inlineinherited 
Set generalized coBüchi acceptance.
num  the number of acceptance sets to use 
The acceptance formula of the form
is generated.
In the case where num is null, the stateacceptance property is automatically turned on.
References spot::acc_cond::acc_code::generalized_co_buchi().

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#namedproperties for a list of named properties used by Spot.

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#namedproperties for a list of named properties used by Spot.

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#namedproperties for a list of named properties used by Spot.

inline 
Return the marks associated to a state if the acceptance is statebased.
References spot::digraph< State_Data, Edge_Data >::out().

inline 
Tell if a state is accepting.
This makes only sense for automata using statebased acceptance, and a simple acceptance condition like Büchi or coBüchi.

inline 
Tell if a state is accepting.
This makes only sense for automata using statebased acceptance, and a simple acceptance condition like Büchi or coBüchi.
References spot::digraph< State_Data, Edge_Data >::out().

inlineinherited 
Build an iterable over the successors of s.
This is meant to be used as
and the above loop is in fact syntactic sugar for

inlineoverridevirtual 
Get an iterator over the successors of local_state.
The iterator has been allocated with new
. It is the responsability of the caller to delete
it when no longer needed.
Implements spot::twa.
References spot::digraph< State_Data, Edge_Data >::is_valid_edge().

inherited 
Unregister an atomic proposition.
num  the BDD variable number returned by register_ap(). 

inherited 

protectedinherited 
BDD dictionary used by the automaton.

mutableprotectedinherited 
Any iterator returned via release_iter.