spot 2.12.2
Functions

Functions

int spot::containment_select_version (const char *version=nullptr)
 
twa_word_ptr spot::difference_word_forq (const_twa_graph_ptr left, const_twa_graph_ptr right)
 Returns a word accepted by left that is rejected by right, or nullptr. More...
 
bool spot::contains_forq (const_twa_graph_ptr left, const_twa_graph_ptr right)
 Returns a boolean value indicating whether the language of left includes in the language of right. More...
 
bool spot::contains (const_twa_graph_ptr left, const_twa_ptr right)
 Test if the language of right is included in that of left. More...
 
bool spot::contains (const_twa_graph_ptr left, formula right)
 Test if the language of right is included in that of left. More...
 
bool spot::contains (formula left, const_twa_ptr right)
 Test if the language of right is included in that of left. More...
 
bool spot::contains (formula left, formula right)
 Test if the language of right is included in that of left. More...
 
bool spot::are_equivalent (const_twa_graph_ptr left, const_twa_graph_ptr right)
 Test if the language of left is equivalent to that of right. More...
 
bool spot::are_equivalent (const_twa_graph_ptr left, formula right)
 Test if the language of left is equivalent to that of right. More...
 
bool spot::are_equivalent (formula left, const_twa_graph_ptr right)
 Test if the language of left is equivalent to that of right. More...
 
bool spot::are_equivalent (formula left, formula right)
 Test if the language of left is equivalent to that of right. More...
 

Detailed Description

Function Documentation

◆ are_equivalent() [1/4]

bool spot::are_equivalent ( const_twa_graph_ptr  left,
const_twa_graph_ptr  right 
)

#include <spot/twaalgos/contains.hh>

Test if the language of left is equivalent to that of right.

Both arguments can be either formulas or automata. Formulas will be converted into automata.

◆ are_equivalent() [2/4]

bool spot::are_equivalent ( const_twa_graph_ptr  left,
formula  right 
)

#include <spot/twaalgos/contains.hh>

Test if the language of left is equivalent to that of right.

Both arguments can be either formulas or automata. Formulas will be converted into automata.

◆ are_equivalent() [3/4]

bool spot::are_equivalent ( formula  left,
const_twa_graph_ptr  right 
)

#include <spot/twaalgos/contains.hh>

Test if the language of left is equivalent to that of right.

Both arguments can be either formulas or automata. Formulas will be converted into automata.

◆ are_equivalent() [4/4]

bool spot::are_equivalent ( formula  left,
formula  right 
)

#include <spot/twaalgos/contains.hh>

Test if the language of left is equivalent to that of right.

Both arguments can be either formulas or automata. Formulas will be converted into automata.

◆ containment_select_version()

int spot::containment_select_version ( const char *  version = nullptr)

#include <spot/twaalgos/contains.hh>

Query, or change the version of the containment check to use by contains() or twa::exclusive_run().

By default those containment checks use a complementation-based algorithm that is generic that work on any acceptance condition. Alternative algorithms such as contains_forq() are available, for Büchi automata, but are not used by default.

When calling this function version can be:

  • "default" to force the above default containment checks to be used
  • "forq" to use contains_forq() when possible
  • nullptr do not modify the preference.

If the first call to containement_select_version() is done with nullptr as an argument, then the value of the SPOT_CONTAINMENT_CHECK environment variable is used instead.

In all cases, the preferred containment check is returned as an integer. This integer is meant to be used by Spot's algorithms to select the desired containment check to apply, but it's encoding (currently 1 for FORQ, 0 for default) should be regarded as an implementation detail subject to change.

◆ contains() [1/4]

bool spot::contains ( const_twa_graph_ptr  left,
const_twa_ptr  right 
)

#include <spot/twaalgos/contains.hh>

Test if the language of right is included in that of left.

Both arguments can be either formulas or automata. Formulas will be converted into automata.

The inclusion check if performed by ensuring that the automaton associated to right does not intersect the automaton associated to the complement of left. It helps if left is a deterministic automaton or a formula (because in both cases complementation is easier).

Complementation is only supported on twa_graph automata, so that is the reason left must be a twa_graph. Right will be explored on-the-fly if it is not a twa_graph.

◆ contains() [2/4]

bool spot::contains ( const_twa_graph_ptr  left,
formula  right 
)

#include <spot/twaalgos/contains.hh>

Test if the language of right is included in that of left.

Both arguments can be either formulas or automata. Formulas will be converted into automata.

The inclusion check if performed by ensuring that the automaton associated to right does not intersect the automaton associated to the complement of left. It helps if left is a deterministic automaton or a formula (because in both cases complementation is easier).

Complementation is only supported on twa_graph automata, so that is the reason left must be a twa_graph. Right will be explored on-the-fly if it is not a twa_graph.

◆ contains() [3/4]

bool spot::contains ( formula  left,
const_twa_ptr  right 
)

#include <spot/twaalgos/contains.hh>

Test if the language of right is included in that of left.

Both arguments can be either formulas or automata. Formulas will be converted into automata.

The inclusion check if performed by ensuring that the automaton associated to right does not intersect the automaton associated to the complement of left. It helps if left is a deterministic automaton or a formula (because in both cases complementation is easier).

Complementation is only supported on twa_graph automata, so that is the reason left must be a twa_graph. Right will be explored on-the-fly if it is not a twa_graph.

◆ contains() [4/4]

bool spot::contains ( formula  left,
formula  right 
)

#include <spot/twaalgos/contains.hh>

Test if the language of right is included in that of left.

Both arguments can be either formulas or automata. Formulas will be converted into automata.

The inclusion check if performed by ensuring that the automaton associated to right does not intersect the automaton associated to the complement of left. It helps if left is a deterministic automaton or a formula (because in both cases complementation is easier).

Complementation is only supported on twa_graph automata, so that is the reason left must be a twa_graph. Right will be explored on-the-fly if it is not a twa_graph.

◆ contains_forq()

bool spot::contains_forq ( const_twa_graph_ptr  left,
const_twa_graph_ptr  right 
)

#include <spot/twaalgos/forq_contains.hh>

Returns a boolean value indicating whether the language of left includes in the language of right.

This implements a FORQ-based language containment algorithm to check whether L(left)⊇L(right). [17]

Precondition
Automata left and right should be non-alternating Büchi-automata.

◆ difference_word_forq()

twa_word_ptr spot::difference_word_forq ( const_twa_graph_ptr  left,
const_twa_graph_ptr  right 
)

#include <spot/twaalgos/forq_contains.hh>

Returns a word accepted by left that is rejected by right, or nullptr.

This implements a FORQ-based language containment algorithm [17] to check whether L(left)⊆L(right), in which case, it returns nullptr. Otherwise, it returns a counterexample, i.e., a word that is accepted by $L(left)\setminus L(right)$, hence the name of the function.

Precondition
Automata left and right should be non-alternating Büchi-automata.

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4