spot  2.6
bool spot::contains (const_twa_graph_ptr left, const_twa_graph_ptr right)
 Test if the language of left is included in that of right. More...
 
bool spot::contains (const_twa_graph_ptr left, formula right)
 Test if the language of left is included in that of right. More...
 
bool spot::contains (formula left, const_twa_graph_ptr right)
 Test if the language of left is included in that of right. More...
 
bool spot::contains (formula left, formula right)
 Test if the language of left is included in that of right. 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.

◆ contains() [1/4]

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

#include <spot/twaalgos/contains.hh>

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

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 left does not intersect the automaton associated to the complement of right. It helps if right is a deterministic automaton or a formula (because in both cases complementation is easier).

◆ contains() [2/4]

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

#include <spot/twaalgos/contains.hh>

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

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 left does not intersect the automaton associated to the complement of right. It helps if right is a deterministic automaton or a formula (because in both cases complementation is easier).

◆ contains() [3/4]

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

#include <spot/twaalgos/contains.hh>

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

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 left does not intersect the automaton associated to the complement of right. It helps if right is a deterministic automaton or a formula (because in both cases complementation is easier).

◆ contains() [4/4]

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

#include <spot/twaalgos/contains.hh>

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

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 left does not intersect the automaton associated to the complement of right. It helps if right is a deterministic automaton or a formula (because in both cases complementation is easier).


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