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

Check containment between LTL formulae. More...

#include <spot/tl/contain.hh>

Collaboration diagram for spot::language_containment_checker:
Collaboration graph

Public Member Functions

 language_containment_checker (const bdd_dict_ptr &dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx)
 
void clear ()
 Clear the cache. More...
 
bool contained (formula l, formula g)
 Check whether L(l) is a subset of L(g). More...
 
bool neg_contained (formula l, formula g)
 Check whether L(!l) is a subset of L(g). More...
 
bool contained_neg (formula l, formula g)
 Check whether L(l) is a subset of L(!g). More...
 
bool equal (formula l, formula g)
 Check whether L(l) = L(g). More...
 

Protected Member Functions

bool incompatible_ (record_ *l, record_ *g)
 
record_ * register_formula_ (formula f)
 

Protected Attributes

bdd_dict_ptr dict_
 
bool exprop_
 
bool symb_merge_
 
bool branching_postponement_
 
bool fair_loop_approx_
 
trans_map translated_
 

Detailed Description

Check containment between LTL formulae.

Constructor & Destructor Documentation

spot::language_containment_checker::language_containment_checker ( const bdd_dict_ptr &  dict,
bool  exprop,
bool  symb_merge,
bool  branching_postponement,
bool  fair_loop_approx 
)

This class uses spot::ltl_to_tgba_fm to translate LTL formulae. See that function for the meaning of these options.

Member Function Documentation

void spot::language_containment_checker::clear ( )

Clear the cache.

bool spot::language_containment_checker::contained ( formula  l,
formula  g 
)

Check whether L(l) is a subset of L(g).

bool spot::language_containment_checker::contained_neg ( formula  l,
formula  g 
)

Check whether L(l) is a subset of L(!g).

bool spot::language_containment_checker::equal ( formula  l,
formula  g 
)

Check whether L(l) = L(g).

bool spot::language_containment_checker::neg_contained ( formula  l,
formula  g 
)

Check whether L(!l) is a subset of L(g).


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 Jul 11 2016 09:54:35 for spot by doxygen 1.8.8