"Semi-internal" class used to implement ltlf_to_mtdfa() More...

#include <spot/twaalgos/ltlf2dfa.hh>

Collaboration diagram for spot::ltlf_translator:

Public Member Functions
	ltlf_translator (const bdd_dict_ptr &dict, bool simplify_terms=true)
	Construct the translator with the given BDD dictionary.

mtdfa_ptr	ltlf_to_mtdfa (formula f, bool fuse_same_bdds, bool detect_empty_univ=true, bool preserve_quantifiers_in_names=false)
	Translate an LTLf formula to a Multi-Terminal DFA.

mtdfa_ptr	ltlf_to_mtdfa_synthesis (formula f, bool fuse_same_bdds, bool detect_empty_univ=true, const std::vector< std::string > *outvars=nullptr, bool do_backprop=false, bool realizability=false, bool one_step_preprocess=false, bool bfs=true, bool terminating_semantics=true, bool preserve_quantifiers_in_names=false)
	Translate an LTLf formula to MTdfa for synthesis.

bdd	ltlf_to_mtbdd (formula f)
	Convert an LTLf formula to an MTBDD.

std::pair< formula, bool >	leaf_to_formula (int b, int term) const
	Convert a leaf value to a formula.

formula	terminal_to_formula (int t) const
	Convert a terminal integer to a formula.

int	formula_to_int (formula f)
	Convert a formula to an integer key.

int	formula_to_terminal (formula f, bool may_stop=false)
	Convert a formula to a terminal index.

bdd	formula_to_terminal_bdd (formula f, bool may_stop=false)
	Convert a formula to a terminal BDD.

int	formula_to_terminal_bdd_as_int (formula f, bool may_stop=false)
	Convert a formula to a terminal BDD integer.

bdd	combine_and (bdd left, bdd right)
	Combine two BDDs with logical AND.

bdd	combine_or (bdd left, bdd right)
	Combine two BDDs with logical OR.

bdd	combine_implies (bdd left, bdd right)
	Combine two BDDs with implication.

bdd	combine_equiv (bdd left, bdd right)
	Combine two BDDs with equivalence.

bdd	combine_xor (bdd left, bdd right)
	Combine two BDDs with exclusive OR.

bdd	combine_not (bdd b)
	Negate a BDD.

bdd	propeq_encode (formula f)
	Encode a formula using propositional equivalences.

formula	propeq_representative (formula f)
	Get the representative for a propositional equiv.

int	formula_propeq_to_int (formula f)
	Convert propositional equiv formula to int.

int	formula_propeq_to_terminal_bdd_as_int (formula f, bool may_stop)
	Convert propositional equiv formula to terminal BDD int.

int	formula_propeq_to_terminal (formula f, bool may_stop=false)
	Convert propositional equiv formula to terminal.

bddExtCache *	get_cache ()
	Return a pointer to the internal BDD cache.

Detailed Description

"Semi-internal" class used to implement ltlf_to_mtdfa()

It is public only to make it possible to demonstrate the inner working of the translation. Do not rely on the interface to be stable.

Constructor & Destructor Documentation

◆ ltlf_translator()

spot::ltlf_translator::ltlf_translator	(	const bdd_dict_ptr &	dict,
		bool	simplify_terms = `true`
	)

Construct the translator with the given BDD dictionary.

Member Function Documentation

◆ combine_and()

bdd spot::ltlf_translator::combine_and	(	bdd	left,
		bdd	right
	)

Combine two BDDs with logical AND.

◆ combine_equiv()

bdd spot::ltlf_translator::combine_equiv	(	bdd	left,
		bdd	right
	)

Combine two BDDs with equivalence.

◆ combine_implies()

bdd spot::ltlf_translator::combine_implies	(	bdd	left,
		bdd	right
	)

Combine two BDDs with implication.

◆ combine_not()

bdd spot::ltlf_translator::combine_not ( bdd b )

Negate a BDD.

◆ combine_or()

bdd spot::ltlf_translator::combine_or	(	bdd	left,
		bdd	right
	)

Combine two BDDs with logical OR.

◆ combine_xor()

bdd spot::ltlf_translator::combine_xor	(	bdd	left,
		bdd	right
	)

Combine two BDDs with exclusive OR.

◆ formula_propeq_to_int()

int spot::ltlf_translator::formula_propeq_to_int ( formula f )

Convert propositional equiv formula to int.

◆ formula_propeq_to_terminal()

int spot::ltlf_translator::formula_propeq_to_terminal	(	formula	f,
		bool	may_stop = `false`
	)

Convert propositional equiv formula to terminal.

◆ formula_propeq_to_terminal_bdd_as_int()

int spot::ltlf_translator::formula_propeq_to_terminal_bdd_as_int	(	formula	f,
		bool	may_stop
	)

Convert propositional equiv formula to terminal BDD int.

◆ formula_to_int()

int spot::ltlf_translator::formula_to_int ( formula f )

Convert a formula to an integer key.

◆ formula_to_terminal()

int spot::ltlf_translator::formula_to_terminal	(	formula	f,
		bool	may_stop = `false`
	)

Convert a formula to a terminal index.

◆ formula_to_terminal_bdd()

bdd spot::ltlf_translator::formula_to_terminal_bdd	(	formula	f,
		bool	may_stop = `false`
	)

Convert a formula to a terminal BDD.

◆ formula_to_terminal_bdd_as_int()

int spot::ltlf_translator::formula_to_terminal_bdd_as_int	(	formula	f,
		bool	may_stop = `false`
	)

Convert a formula to a terminal BDD integer.

◆ get_cache()

bddExtCache * spot::ltlf_translator::get_cache ( )

inline

Return a pointer to the internal BDD cache.

◆ leaf_to_formula()

std::pair< formula, bool > spot::ltlf_translator::leaf_to_formula	(	int	b,
		int	term
	)		const

Convert a leaf value to a formula.

◆ ltlf_to_mtbdd()

bdd spot::ltlf_translator::ltlf_to_mtbdd ( formula f )

Convert an LTLf formula to an MTBDD.

◆ ltlf_to_mtdfa()

mtdfa_ptr spot::ltlf_translator::ltlf_to_mtdfa	(	formula	f,
		bool	fuse_same_bdds,
		bool	detect_empty_univ = `true`,
		bool	preserve_quantifiers_in_names = `false`
	)

Translate an LTLf formula to a Multi-Terminal DFA.

◆ ltlf_to_mtdfa_synthesis()

mtdfa_ptr spot::ltlf_translator::ltlf_to_mtdfa_synthesis	(	formula	f,
		bool	fuse_same_bdds,
		bool	detect_empty_univ = `true`,
		const std::vector< std::string > *	outvars = `nullptr`,
		bool	do_backprop = `false`,
		bool	realizability = `false`,
		bool	one_step_preprocess = `false`,
		bool	bfs = `true`,
		bool	terminating_semantics = `true`,
		bool	preserve_quantifiers_in_names = `false`
	)

Translate an LTLf formula to MTdfa for synthesis.

◆ propeq_encode()

bdd spot::ltlf_translator::propeq_encode ( formula f )

Encode a formula using propositional equivalences.

◆ propeq_representative()

formula spot::ltlf_translator::propeq_representative ( formula f )

Get the representative for a propositional equiv.

◆ terminal_to_formula()

formula spot::ltlf_translator::terminal_to_formula ( int t ) const

Convert a terminal integer to a formula.

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

spot/twaalgos/ltlf2dfa.hh

Public Member Functions