spot  2.3.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Public Member Functions | Static Public Member Functions | Protected Attributes | List of all members
spot::twa_product Class Reference

A lazy product. (States are computed on the fly.) More...

#include <spot/twa/twaproduct.hh>

Inheritance diagram for spot::twa_product:
Inheritance graph
Collaboration diagram for spot::twa_product:
Collaboration graph

Public Member Functions

 twa_product (const const_twa_ptr &left, const const_twa_ptr &right)
 Constructor. More...
 
virtual const stateget_init_state () const override
 Get the initial state of the automaton. More...
 
virtual twa_succ_iteratorsucc_iter (const state *state) const override
 Get an iterator over the successors of local_state. More...
 
virtual std::string format_state (const state *state) const override
 Format the state as a string for printing. More...
 
virtual stateproject_state (const state *s, const const_twa_ptr &t) const override
 Project a state on an automaton. More...
 
const acc_condleft_acc () const
 
const acc_condright_acc () const
 
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 be register 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 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...
 
unsigned num_sets () const
 Number of acceptance sets used by the automaton. More...
 
const acc_cond::acc_codeget_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 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...
 
acc_cond::mark_t set_buchi ()
 Set 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" proeprty. 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_deterministic () const
 Whether the automaton is deterministic. More...
 
void prop_deterministic (trival val)
 Set the deterministic property. More...
 
trival prop_unambiguous () const
 Whether the automaton is unambiguous. More...
 
void prop_unambiguous (trival val)
 Sets the unambiguous property. More...
 
trival prop_semi_deterministic () const
 Whether the automaton is semi-deterministic. More...
 
void prop_semi_deterministic (trival val)
 Sets 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_condacc () const
 The acceptance condition of the automaton. More...
 
acc_condacc ()
 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 Attributes

const_twa_ptr left_
 
const_twa_ptr right_
 
bool left_kripke_
 
fixed_size_pool pool_
 
twa_succ_iteratoriter_cache_
 Any iterator returned via release_iter. More...
 
bdd_dict_ptr dict_
 BDD dictionary used by the automaton. More...
 

Detailed Description

A lazy product. (States are computed on the fly.)

Constructor & Destructor Documentation

spot::twa_product::twa_product ( const const_twa_ptr &  left,
const const_twa_ptr &  right 
)

Constructor.

Parameters
leftThe left automata in the product.
rightThe right automata in the product. Do not be fooled by these arguments: a product is commutative.

Member Function Documentation

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

The acceptance condition of the automaton.

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

The acceptance condition of the automaton.

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

Return an accepting run if one exists.

Note that this method currently only works for Fin-less 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.

virtual twa_word_ptr spot::twa::accepting_word ( ) const
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.

static prop_set spot::twa::all ( )
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:

aut->prop_copy(other_aut, {true, 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 deterministic, 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 do not fall into any of
these groups, we will be forced to review all algorithm 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 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}

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.

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

The vector of atomic propositions registered by this automaton.

bdd spot::twa::ap_vars ( ) const
inlineinherited

The set of atomic propositions as a conjunction.

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

Copy the acceptance condition of another TωA.

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

Copy the atomic propositions of another TωA.

virtual std::string spot::twa_product::format_state ( const state s) const
overridevirtual

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.

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

Acceptance formula used by the automaton.

bdd_dict_ptr spot::twa::get_dict ( ) const
inlineinherited

Get the dictionary associated to the automaton.

Automata are labeled by Boolean formulas over atomic propositions. These Boolean formula 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.

virtual const state* spot::twa_product::get_init_state ( ) const
overridevirtual

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.

Reimplemented in spot::twa_product_init, and spot::tgta_product.

template<typename T >
T* spot::twa::get_named_prop ( std::string  s) const
inlineinherited

Retrieve a named property.

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

Parameters
sthe name of the object to retrieve
Template Parameters
Tthe 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.

template<typename T >
T* spot::twa::get_or_set_named_prop ( std::string  s)
inlineinherited

Create or retrieve a named property.

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

This function create a property object of a given type, and attached it to name if not such property exist, or it returns

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

virtual twa_run_ptr spot::twa::intersecting_run ( const_twa_ptr  other,
bool  from_other = false 
) const
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 Fin-less 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.

virtual twa_word_ptr spot::twa::intersecting_word ( const_twa_ptr  other) const
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.

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

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

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

Check whether the language of the automaton is empty.

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

trival spot::twa::is_sba ( ) const
inlineinherited

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

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

unsigned spot::twa::num_sets ( ) const
inlineinherited

Number of acceptance sets used by the automaton.

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

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

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 from spot::twa.

trival spot::twa::prop_deterministic ( ) const
inlineinherited

Whether the automaton is deterministic.

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

See also
prop_unambiguous()
is_deterministic()
void spot::twa::prop_deterministic ( trival  val)
inlineinherited

Set the deterministic property.

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

See also
prop_unambiguous()
prop_semi_deterministic()
trival spot::twa::prop_inherently_weak ( ) const
inlineinherited

Whether the automaton is inherently weak.

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

See also
prop_weak()
prop_terminal()
void spot::twa::prop_inherently_weak ( trival  val)
inlineinherited

Set the "inherently weak" proeprty.

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

See also
prop_weak()
prop_terminal()
trival spot::twa::prop_semi_deterministic ( ) const
inlineinherited

Whether the automaton is semi-deterministic.

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

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_deterministic()
is_semi_deterministic()
void spot::twa::prop_semi_deterministic ( trival  val)
inlineinherited

Sets the semi-deterministic property.

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

See also
prop_deterministic()
trival spot::twa::prop_state_acc ( ) const
inlineinherited

Whether the automaton uses state-based acceptance.

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

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

Set the state-based-acceptance property.

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

trival spot::twa::prop_stutter_invariant ( ) const
inlineinherited

Whether the automaton is stutter-invariant.

An automaton is stutter-invariant iff any accepted word remains accepted after removing a finite number of duplicate letters, or after duplicating 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 one using of the the is_stutter_invariant() function.

See also
is_stutter_invariant
void spot::twa::prop_stutter_invariant ( trival  val)
inlineinherited

Set the stutter-invariant property.

trival spot::twa::prop_terminal ( ) const
inlineinherited

Whether the automaton is terminal.

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

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

See also
prop_weak()
prop_inherently_weak()
void spot::twa::prop_terminal ( trival  val)
inlineinherited

Set the terminal property.

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

See also
prop_weak()
prop_inherently_weak()
trival spot::twa::prop_unambiguous ( ) const
inlineinherited

Whether the automaton is unambiguous.

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

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

See also
prop_deterministic()
is_unambiguous()
void spot::twa::prop_unambiguous ( trival  val)
inlineinherited

Sets the unambiguous property.

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

See also
prop_deterministic()
trival spot::twa::prop_very_weak ( ) const
inlineinherited

Whether the automaton is very-weak.

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

See also
prop_terminal()
prop_weak()
void spot::twa::prop_very_weak ( trival  val)
inlineinherited

Set the very-weak property.

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

See also
prop_terminal()
prop_weak()
trival spot::twa::prop_weak ( ) const
inlineinherited

Whether the automaton is weak.

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

See also
prop_terminal()
prop_inherently_weak()
void spot::twa::prop_weak ( trival  val)
inlineinherited

Set the weak property.

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

See also
prop_terminal()
prop_inherently_weak()
int spot::twa::register_ap ( formula  ap)
inlineinherited

Register an atomic proposition designated by ap.

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

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

Returns
The BDD variable number assigned for this atomic proposition.
int spot::twa::register_ap ( std::string  ap)
inlineinherited

Register an atomic proposition designated by ap.

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

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

Returns
The BDD variable number assigned for this atomic proposition.

References spot::formula::ap().

void spot::twa::register_aps_from_dict ( )
inlineinherited

Register all atomic propositions that have already be register 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 proposition 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.

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

Release an iterator after usage.

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

void spot::twa::release_named_properties ( )
inlineinherited

Destroy all named properties.

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

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

Set the acceptance condition of the automaton.

Parameters
numthe number of acceptance sets used
cthe acceptance formula
acc_cond::mark_t spot::twa::set_buchi ( )
inlineinherited

Set Büchi acceptance.

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

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

in addition.

See also
prop_state_acc
void spot::twa::set_generalized_buchi ( unsigned  num)
inlineinherited

Set generalized Büchi acceptance.

Parameters
numthe number of acceptance sets to used

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.

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

Declare a named property.

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

This function attaches the object val to the current automaton, under the name s and destroy 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.

template<typename T >
void spot::twa::set_named_prop ( std::string  s,
T *  val 
)
inlineinherited

Declare a named property.

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

This function attaches the object val to the current automaton, under the name s and destroy 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.

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

Erase a named property.

Arbitrary objects can be attached to automata. Those are called named properties. They are used for instance to name all the state 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.

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

Build an iterable over the successors of s.

This is meant to be used as

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

and the above loop is in fact syntactic sugar for

twa_succ_iterator* i = aut->succ_iter(s);
if (i->first())
do
{
// use i->cond(), i->acc(), i->dst()
}
while (i->next());
aut->release_iter(i);
virtual twa_succ_iterator* spot::twa_product::succ_iter ( const state local_state) const
overridevirtual

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.

See also
succ()

Implements spot::twa.

Reimplemented in spot::tgta_product.

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

Unregister an atomic proposition.

Parameters
numthe BDD variable number returned by register_ap().

Member Data Documentation

bdd_dict_ptr spot::twa::dict_
protectedinherited

BDD dictionary used by the automaton.

twa_succ_iterator* spot::twa::iter_cache_
mutableprotectedinherited

Any iterator returned via release_iter.


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

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Feb 20 2017 07:08:26 for spot by doxygen 1.8.8