"Semi-internal" for translating LTL using MTBDDs More...

#include <spot/twaalgos/mtdswa.hh>

Collaboration diagram for spot::simple_ltl_translator:

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

mtdswa_ptr	ltl_to_mtdswa (formula f, bool fuse_same_bdds)
	Translate an LTL formula to an MTDSwA.

mtdswa_ptr	ltl_to_mtdswa_synthesis (formula f, const std::vector< std::string > &outvars, bool realizability, int debug=-1)
	Translate an LTL formula for synthesis to MTDSwA.

bdd	ltl_to_mtbdd (formula f)
	Convert an LTL formula to an MTBDD.

formula	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_propeq_to_int (formula f)
	Convert a propositional equivalence formula to int.

int	formula_to_terminal (formula f)
	Convert a formula to a terminal index.

bdd	formula_to_terminal_bdd (formula f)
	Convert a formula to a terminal BDD.

int	formula_to_terminal_bdd_as_int (formula f)
	Convert a formula to a terminal BDD integer.

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

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 logical implication.

bdd	combine_equiv (bdd left, bdd right)
	Combine two BDDs with logical 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, int level=0)
	Encode a formula using propositional equivalences.

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

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

Detailed Description

"Semi-internal" for translating LTL using MTBDDs

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

◆ simple_ltl_translator()

spot::simple_ltl_translator::simple_ltl_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::simple_ltl_translator::combine_and	(	bdd	left,
		bdd	right
	)

Combine two BDDs with logical AND.

◆ combine_equiv()

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

Combine two BDDs with logical equivalence.

◆ combine_implies()

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

Combine two BDDs with logical implication.

◆ combine_not()

bdd spot::simple_ltl_translator::combine_not ( bdd b )

Negate a BDD.

◆ combine_or()

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

Combine two BDDs with logical OR.

◆ combine_xor()

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

Combine two BDDs with exclusive OR.

◆ formula_propeq_to_int()

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

Convert a propositional equivalence formula to int.

◆ formula_propeq_to_terminal_bdd_as_int()

int spot::simple_ltl_translator::formula_propeq_to_terminal_bdd_as_int ( formula f )

Convert propositional equiv formula to terminal BDD int.

◆ formula_to_int()

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

Convert a formula to an integer key.

◆ formula_to_terminal()

int spot::simple_ltl_translator::formula_to_terminal ( formula f )

Convert a formula to a terminal index.

◆ formula_to_terminal_bdd()

bdd spot::simple_ltl_translator::formula_to_terminal_bdd ( formula f )

Convert a formula to a terminal BDD.

◆ formula_to_terminal_bdd_as_int()

int spot::simple_ltl_translator::formula_to_terminal_bdd_as_int ( formula f )

Convert a formula to a terminal BDD integer.

◆ get_cache()

bddExtCache * spot::simple_ltl_translator::get_cache ( )

inline

Return a pointer to the internal BDD cache.

◆ leaf_to_formula()

formula spot::simple_ltl_translator::leaf_to_formula	(	int	b,
		int	term
	)		const

Convert a leaf value to a formula.

◆ ltl_to_mtbdd()

bdd spot::simple_ltl_translator::ltl_to_mtbdd ( formula f )

Convert an LTL formula to an MTBDD.

◆ ltl_to_mtdswa()

mtdswa_ptr spot::simple_ltl_translator::ltl_to_mtdswa	(	formula	f,
		bool	fuse_same_bdds
	)

Translate an LTL formula to an MTDSwA.

◆ ltl_to_mtdswa_synthesis()

mtdswa_ptr spot::simple_ltl_translator::ltl_to_mtdswa_synthesis	(	formula	f,
		const std::vector< std::string > &	outvars,
		bool	realizability,
		int	debug = `-1`
	)

Translate an LTL formula for synthesis to MTDSwA.

◆ propeq_encode()

bdd spot::simple_ltl_translator::propeq_encode	(	formula	f,
		int	level = `0`
	)

Encode a formula using propositional equivalences.

◆ propeq_representative()

formula spot::simple_ltl_translator::propeq_representative	(	formula	f,
		bool	isacc
	)

Get the representative formula for a propositional equiv.

◆ terminal_to_formula()

formula spot::simple_ltl_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/mtdswa.hh

Public Member Functions