spot
2.10.6

Interface for a Kripke structure. More...
#include <spot/kripke/kripke.hh>
Public Member Functions  
kripke (const bdd_dict_ptr &d)  
virtual acc_cond::mark_t  state_acceptance_mark (const state *) const override 
The acceptance mark that labels state s. More...  
virtual bdd  state_condition (const state *s) const =0 
The condition that label the state s. More...  
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 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...  
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  
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_ 
Interface for a Kripke structure.
A Kripke structure is a graph in which each node (=state) is labeled by a conjunction of atomic proposition.
Such a structure can be seen as spot::tgba without any acceptance condition.
A programmer that develops an instance of Kripke structure needs just provide an implementation for the following methods:
The other methods of the tgba interface (like those dealing with acceptance conditions) are supplied by this kripke class and need not be defined.
See also spot::kripke_succ_iterator.

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.

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.

pure virtualinherited 
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.
Implemented in spot::twa_product, spot::twa_graph, spot::kripke_graph, spot::taa_tgba_labelled< label >, spot::taa_tgba_labelled< std::string >, spot::taa_tgba_labelled< formula >, and spot::tgta_explicit.

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.

pure virtualinherited 
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.
Implemented in spot::taa_tgba, spot::twa_product_init, spot::twa_product, spot::twa_graph, spot::tgta_product, spot::tgta_explicit, and spot::kripke_graph.

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.

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

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

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.

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

pure virtualinherited 
The condition that label the state s.
This should be a conjunction of atomic propositions.
Implemented in spot::kripke_graph.

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

pure virtualinherited 
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.
Implemented in spot::twa_product, spot::twa_graph, spot::tgta_product, spot::taa_tgba, spot::kripke_graph, and spot::tgta_explicit.

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.