spot::language_containment_checker Class Reference

#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)
	Test whether two cached formulas are incompatible.
record_ *	register_formula_ (formula f)
	Register a formula in the translation cache.

Protected Attributes
bdd_dict_ptr	dict_
	Dictionary used for translations.
bool	exprop_
	Use existential properties.
bool	symb_merge_
	Merge symbolic states.
bool	branching_postponement_
	Postpone branching choices.
bool	fair_loop_approx_
	Approximate fair loops.
trans_map_ *	translated_
	Translation cache.
tl_simplifier_cache *	c_
std::unique_ptr< const output_aborter >	aborter_ = nullptr
	Optional output aborter.

Detailed Description

Check containment between LTL formulas.

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 an LTL-to-TGBA translation to translate LTL formulas. See that function for the meaning of these options.

References spot::make_bdd_dict().

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

incompatible_()

bool spot::language_containment_checker::incompatible_ ( record_ *  l, record_ *  g  )

protected

Test whether two cached formulas are incompatible.

neg_contained()

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

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

register_formula_()

record_ * spot::language_containment_checker::register_formula_ ( formula  f )

protected

Register a formula in the translation cache.

Member Data Documentation

aborter_

std::unique_ptr<const output_aborter> spot::language_containment_checker::aborter_ = nullptr

protected

Optional output aborter.

branching_postponement_

bool spot::language_containment_checker::branching_postponement_

protected

Postpone branching choices.

c_

tl_simplifier_cache* spot::language_containment_checker::c_

protected

Formula simplifier cache.

dict_

bdd_dict_ptr spot::language_containment_checker::dict_

protected

Dictionary used for translations.

exprop_

bool spot::language_containment_checker::exprop_

protected

Use existential properties.

fair_loop_approx_

bool spot::language_containment_checker::fair_loop_approx_

protected

Approximate fair loops.

symb_merge_

bool spot::language_containment_checker::symb_merge_

protected

Merge symbolic states.

translated_

trans_map_* spot::language_containment_checker::translated_

protected

Translation cache.

---

The documentation for this class was generated from the following file:

• spot/tl/contain.hh