spot
2.7.5

Kripke Structure. More...
#include <spot/kripke/kripkegraph.hh>
Public Types  
typedef digraph< kripke_graph_state, void >  graph_t 
typedef internal::edge_storage< unsigned, unsigned, unsigned, internal::boxed_label< void, true > >  edge_storage_t 
typedef internal::distate_storage< unsigned, internal::boxed_label< kripke_graph_state, false > >  state_storage_t 
typedef std::vector< state_storage_t >  state_vector 
typedef unsigned  state_num 
Public Member Functions  
kripke_graph (const bdd_dict_ptr &d)  
unsigned  num_states () const 
unsigned  num_edges () const 
void  set_init_state (state_num s) 
state_num  get_init_state_number () const 
virtual const kripke_graph_state *  get_init_state () const override 
Get the initial state of the automaton. More...  
virtual kripke_graph_succ_iterator< graph_t > *  succ_iter (const spot::state *st) const override 
Allow to get an iterator on the state we passed in parameter. More...  
state_num  state_number (const state *st) const 
const kripke_graph_state *  state_from_number (state_num n) const 
kripke_graph_state *  state_from_number (state_num n) 
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...  
virtual bdd  state_condition (const state *s) const override 
Get the condition on the state. More...  
edge_storage_t &  edge_storage (unsigned t) 
const edge_storage_t  edge_storage (unsigned t) const 
unsigned  new_state (bdd cond) 
unsigned  new_states (unsigned n, bdd cond) 
unsigned  new_edge (unsigned src, unsigned dst) 
const state_vector &  states () const 
state_vector &  states () 
internal::all_trans< const graph_t >  edges () const noexcept 
internal::all_trans< graph_t >  edges () noexcept 
internal::state_out< const graph_t >  out (unsigned src) const 
internal::state_out< graph_t >  out (unsigned src) 
virtual acc_cond::mark_t  state_acceptance_mark (const state *) const override 
The acceptance mark that labels state s. 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, bool from_other=false) const 
Return an accepting run recognizing a word accepted by two automata. More...  
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  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...  
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...  
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_ 
Kripke Structure.

inlineinherited 
The acceptance condition of the automaton.

inlineinherited 
The acceptance condition of the automaton.
References spot::acc_cond::add_sets(), and spot::acc_cond::num_sets().

virtualinherited 
Return an accepting run if one exists.
Note that this method currently only works for Finless acceptance. For acceptance conditions that contain Fin acceptance, you can either rely on is_empty() and not use any accepting run, or remove Fin acceptance using remove_fin() and compute an accepting run on that larger automaton.
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.

virtualinherited 
Return an accepting word if one exists.
Note that this method DOES works with Fin acceptance.
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.

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.

virtualinherited 
Return an accepting run recognizing a word accepted by exactly one of the two automata.
If from_other is true, the returned run will be over the other automaton. Otherwise, the run will be over this automaton.
Note that this method currently only works if the automaton from which the accepting run is extracted uses Finless acceptance. (The other automaton can have any acceptance condition.)
Return nullptr iff the two automata recognize the same language.

virtualinherited 
Return a word accepted by exactly one of the two automata.
Note that this method DOES works with Fin acceptance.
Return nullptr iff the two automata recognize the same language.

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.
If from_other is true, the returned run will be over the other automaton. Otherwise, the run will be over this automaton.
Note that this method currently only works if the automaton from which the accepting run is extracted uses Finless acceptance. (The other automaton can have any acceptance condition.)
For acceptance conditions that contain Fin acceptance, you can either rely on intersects() and not use any accepting run, or remove Fin acceptance using remove_fin() and compute an intersecting run on this larger automaton.
Return nullptr if no accepting run were found.

virtualinherited 
Return a word accepted by two automata.
Note that this method DOES works with Fin acceptance.
Return nullptr if no accepting word were found.

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

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.

inlineinherited 
Whether this is a statebased Büchi automaton.
An SBA has a Büchi acceptance, and should have its statebased acceptance property set.

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

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

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.

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

inlineinherited 
Set the acceptance condition of the automaton.
num  the number of acceptance sets used 
c  the acceptance formula 
References spot::acc_cond::set_acceptance().

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

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::mark().

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::mark().

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::set_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::set_generalized_co_buchi().

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.

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

overridevirtualinherited 
The acceptance mark that labels state s.
Implements spot::fair_kripke.

inlineoverridevirtual 
Get the condition on the state.
Implements spot::fair_kripke.
References spot::digraph< State_Data, Edge_Data >::edge_storage(), spot::digraph< State_Data, Edge_Data >::edges(), spot::digraph< State_Data, Edge_Data >::new_edge(), spot::digraph< State_Data, Edge_Data >::new_state(), spot::digraph< State_Data, Edge_Data >::new_states(), spot::digraph< State_Data, Edge_Data >::out(), and spot::digraph< State_Data, Edge_Data >::states().

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 
Allow to get an iterator on the state we passed in parameter.
Implements spot::twa.
References spot::digraph< State_Data, Edge_Data >::is_valid_edge(), spot::digraph< State_Data, Edge_Data >::state_data(), and spot::digraph< State_Data, Edge_Data >::state_storage().

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

protectedinherited 
BDD dictionary used by the automaton.

mutableprotectedinherited 
Any iterator returned via release_iter.