spot  2.2.2
 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 (bdd_dict_ptr dict=make_bdd_dict(), bool exprop=false, bool symb_merge=true, bool branching_postponement=false, bool fair_loop_approx=false)
 
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 ( bdd_dict_ptr  dict = make_bdd_dict(),
bool  exprop = false,
bool  symb_merge = true,
bool  branching_postponement = false,
bool  fair_loop_approx = false 
)

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 Fri Dec 16 2016 06:04:09 for spot by doxygen 1.8.8