spot
2.11.3

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...  
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.
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.
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.
#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.
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 onthefly if it is not a twa_graph.
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 onthefly if it is not a twa_graph.
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 onthefly if it is not a twa_graph.
#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 onthefly if it is not a twa_graph.