spot::language_containment_checker Class Reference

Check containment between LTL formulae. More...

#include <spot/tl/contain.hh>

Collaboration diagram for spot::language_containment_checker:

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, unsigned max_states=0U)
void	clear ()
	Clear the cache.
bool	contained (formula l, formula g)
	Check whether L(l) is a subset of L(g).
bool	neg_contained (formula l, formula g)
	Check whether L(!l) is a subset of L(g).
bool	contained_neg (formula l, formula g)
	Check whether L(l) is a subset of L(!g).
bool	equal (formula l, formula g)
	Check whether L(l) = L(g).

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_
tl_simplifier_cache *	c_
std::unique_ptr< const output_aborter >	aborter_ = nullptr

Detailed Description

Check containment between LTL formulae.

Constructor & Destructor Documentation

language_containment_checker()

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,
		unsigned	max_states = 0U
	)

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

Member Function Documentation

clear()

void spot::language_containment_checker::clear

(

)

Clear the cache.

contained()

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

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

contained_neg()

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

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

equal()

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

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

neg_contained()

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:

• spot/tl/contain.hh