Classes
class	spot::acc_cond
	An acceptance condition. More...

class	spot::bdd_dict
	Map BDD variables to formulas. More...

class	spot::bdd_dict_preorder
	A BDD dictionary wrapper that pre-registers atomic propositions before use. More...

class	spot::state
	Abstract class for states. More...

struct	spot::state_ptr_less_than
	Strict Weak Ordering for state pointers. More...

struct	spot::state_ptr_equal
	An Equivalence Relation for state pointers. More...

struct	spot::state_ptr_hash
	Hash Function for state pointers. More...

class	spot::state_unicity_table
	Render state pointers unique via a hash table. More...

struct	spot::state_shared_ptr_less_than
	Strict Weak Ordering for `shared_state`. More...

struct	spot::state_shared_ptr_equal
	An Equivalence Relation for `shared_state`. More...

struct	spot::state_shared_ptr_hash
	Hash Function for `shared_state`. More...

class	spot::twa_succ_iterator
	Iterate over the successors of a state. More...

class	spot::twa
	A Transition-based ω-Automaton. More...

struct	spot::twa_word
	An infinite word stored as a lasso. More...

Typedefs
typedef std::shared_ptr< bdd_dict >	spot::bdd_dict_ptr
	Shared pointer to a bdd_dict.

typedef std::shared_ptr< twa >	spot::twa_ptr
	Shared pointer to a mutable twa.

typedef std::shared_ptr< const twa >	spot::const_twa_ptr
	Shared pointer to a const twa.

typedef std::shared_ptr< const twa_word >	spot::const_twa_word_ptr
	Shared pointer to a const twa_word.

typedef std::shared_ptr< twa_word >	spot::twa_word_ptr
	Shared pointer to a mutable twa_word.

typedef std::shared_ptr< twa_run >	spot::twa_run_ptr
	Shared pointer to a twa_run.

typedef std::shared_ptr< const state >	spot::shared_state
	Shared pointer to a const state.

Functions
bdd_dict_ptr	spot::make_bdd_dict ()
	Create a new, empty bdd_dict wrapped in a shared pointer.

std::ostream &	spot::bdd_print_sat (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as a list of literals.

std::string	spot::bdd_format_sat (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as a list of literals.

std::ostream &	spot::bdd_print_accset (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as a set of acceptance conditions.

std::string	spot::bdd_format_accset (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as a set of acceptance conditions.

std::ostream &	spot::bdd_print_set (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as a set.

std::string	spot::bdd_format_set (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as a set.

std::ostream &	spot::bdd_print_formula (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as a formula.

std::string	spot::bdd_format_formula (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as a formula.

void	spot::enable_utf8 ()
	Enable UTF-8 output for bdd printers.

std::string	spot::bdd_format_isop (const bdd_dict_ptr &dict, bdd b)
	Format a BDD as an irredundant sum of product.

std::ostream &	spot::bdd_print_isop (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
	Print a BDD as an irredundant sum of product.

void	spot::shared_state_deleter (state *s)
	Deleter for shared_state: calls state::destroy().

twa_word_ptr	spot::make_twa_word (const bdd_dict_ptr &dict)
	Create an empty twa_word.

twa_word_ptr	spot::make_twa_word (const twa_run_ptr &run)
	Create a twa_word from a twa_run.

twa_word_ptr	spot::parse_word (const std::string &word, const bdd_dict_ptr &dict)
	Parse a twa_word.

bdd	spot::formula_to_bdd (formula f, const bdd_dict_ptr &d, void *for_me)
	Convert a Boolean formula into a BDD.

template<typename T >
bdd	spot::formula_to_bdd (formula f, const bdd_dict_ptr &d, const std::shared_ptr< T > &for_me)
	Convert a Boolean formula into a BDD.

formula	spot::bdd_to_formula (bdd f, const bdd_dict_ptr d)
	Convert a BDD into a formula.

formula	spot::bdd_to_cnf_formula (bdd f, const bdd_dict_ptr d)
	Convert a BDD into a formula.

Detailed Description

Typedef Documentation

◆ bdd_dict_ptr

typedef std::shared_ptr< bdd_dict > spot::bdd_dict_ptr

#include <spot/twa/bdddict.hh>

Shared pointer to a bdd_dict.

◆ const_twa_ptr

typedef std::shared_ptr<const twa> spot::const_twa_ptr

#include <spot/twa/fwd.hh>

Shared pointer to a const twa.

◆ const_twa_word_ptr

typedef std::shared_ptr<const twa_word> spot::const_twa_word_ptr

#include <spot/twa/fwd.hh>

Shared pointer to a const twa_word.

◆ shared_state

typedef std::shared_ptr<const state> spot::shared_state

#include <spot/twa/twa.hh>

Shared pointer to a const state.

Used in algorithms that manage state ownership via shared pointers rather than raw pointers. Pair with shared_state_deleter to call state::destroy() on deletion.

◆ twa_ptr

typedef std::shared_ptr<twa> spot::twa_ptr

#include <spot/twa/fwd.hh>

Shared pointer to a mutable twa.

◆ twa_run_ptr

typedef std::shared_ptr< twa_run > spot::twa_run_ptr

#include <spot/twa/twa.hh>

Shared pointer to a twa_run.

◆ twa_word_ptr

typedef std::shared_ptr< twa_word > spot::twa_word_ptr

#include <spot/twa/fwd.hh>

Shared pointer to a mutable twa_word.

Function Documentation

◆ bdd_format_accset()

std::string spot::bdd_format_accset	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Format a BDD as a set of acceptance conditions.

This is used when saving a TGBA.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns: The BDD formatted as a string.

◆ bdd_format_formula()

std::string spot::bdd_format_formula	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Format a BDD as a formula.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns: The BDD formatted as a string.

◆ bdd_format_isop()

std::string spot::bdd_format_isop	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Format a BDD as an irredundant sum of product.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns: The BDD formatted as a string.

◆ bdd_format_sat()

std::string spot::bdd_format_sat	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Format a BDD as a list of literals.

This assumes that b is a conjunction of literals.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns: The BDD formatted as a string.

◆ bdd_format_set()

std::string spot::bdd_format_set	(	const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Format a BDD as a set.

Parameters

dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns: The BDD formatted as a string.

◆ bdd_print_accset()

std::ostream & spot::bdd_print_accset	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Print a BDD as a set of acceptance conditions.

This is used when saving a TGBA.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

Returns: The BDD formatted as a string.

◆ bdd_print_formula()

std::ostream & spot::bdd_print_formula	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Print a BDD as a formula.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

◆ bdd_print_isop()

std::ostream & spot::bdd_print_isop	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Print a BDD as an irredundant sum of product.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

◆ bdd_print_sat()

std::ostream & spot::bdd_print_sat	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Print a BDD as a list of literals.

This assumes that b is a conjunction of literals.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

◆ bdd_print_set()

std::ostream & spot::bdd_print_set	(	std::ostream &	os,
		const bdd_dict_ptr &	dict,
		bdd	b
	)

#include <spot/twa/bddprint.hh>

Print a BDD as a set.

Parameters

os	The output stream.
dict	The dictionary to use, to lookup variables.
b	The BDD to print.

◆ bdd_to_cnf_formula()

formula spot::bdd_to_cnf_formula	(	bdd	f,
		const bdd_dict_ptr	d
	)

#include <spot/twa/formula2bdd.hh>

Convert a BDD into a formula.

Format the BDD as a Boolean spot::formula object. This works only for Boolean formulas, and all the BDD variables used in f should have been registered in d. Although the result has type formula, it obviously does not use any temporal operator.

The bdd_to_formula() version produces an irredundant sum of product (see the minato_isop class for details) and map the BDD variables back into their atomic propositions.

The bdd_to_cnf_formula() version produces an irredundant product of sum, using the dual construction.

◆ bdd_to_formula()

formula spot::bdd_to_formula	(	bdd	f,
		const bdd_dict_ptr	d
	)

#include <spot/twa/formula2bdd.hh>

Convert a BDD into a formula.

Format the BDD as a Boolean spot::formula object. This works only for Boolean formulas, and all the BDD variables used in f should have been registered in d. Although the result has type formula, it obviously does not use any temporal operator.

The bdd_to_formula() version produces an irredundant sum of product (see the minato_isop class for details) and map the BDD variables back into their atomic propositions.

The bdd_to_cnf_formula() version produces an irredundant product of sum, using the dual construction.

◆ enable_utf8()

void spot::enable_utf8 ( )

#include <spot/twa/bddprint.hh>

Enable UTF-8 output for bdd printers.

◆ formula_to_bdd() [1/2]

template<typename T >

bdd spot::formula_to_bdd	(	formula	f,
		const bdd_dict_ptr &	d,
		const std::shared_ptr< T > &	for_me
	)

#include <spot/twa/formula2bdd.hh>

Convert a Boolean formula into a BDD.

Convert the Boolean formula f into a BDD, using existing variables from d, and registering new ones as necessary. for_me, the address of the user of these BDD variables will be passed to d when registering the variables.

If you only use the BDD representation temporarily, for instance passing it right away to bdd_to_formula(), you should not forget to unregister the variables that have been registered for for_me. See bdd_dict::unregister_all_my_variables().

References spot::formula_to_bdd().

◆ formula_to_bdd() [2/2]

bdd spot::formula_to_bdd	(	formula	f,
		const bdd_dict_ptr &	d,
		void *	for_me
	)

#include <spot/twa/formula2bdd.hh>

Convert a Boolean formula into a BDD.

Convert the Boolean formula f into a BDD, using existing variables from d, and registering new ones as necessary. for_me, the address of the user of these BDD variables will be passed to d when registering the variables.

If you only use the BDD representation temporarily, for instance passing it right away to bdd_to_formula(), you should not forget to unregister the variables that have been registered for for_me. See bdd_dict::unregister_all_my_variables().

Referenced by spot::formula_to_bdd().

◆ make_bdd_dict()

bdd_dict_ptr spot::make_bdd_dict ( )

inline

#include <spot/twa/bdddict.hh>

Create a new, empty bdd_dict wrapped in a shared pointer.

Referenced by spot::aig::aig(), spot::aig::aig(), spot::language_containment_checker::language_containment_checker(), spot::tl_simplifier::tl_simplifier(), spot::tl_simplifier::tl_simplifier(), spot::translator::translator(), spot::aig::parse_aag(), spot::aig::parse_aag(), spot::aig::parse_aag(), spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::setup(), and spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::setup().

◆ make_twa_word() [1/2]

twa_word_ptr spot::make_twa_word ( const bdd_dict_ptr & dict )

inline

#include <spot/twaalgos/word.hh>

Create an empty twa_word.

Note that empty twa_word are invalid and cannot be printed. After creating an empty twa_word, you should at least populate the cycle.

◆ make_twa_word() [2/2]

twa_word_ptr spot::make_twa_word ( const twa_run_ptr & run )

inline

#include <spot/twaalgos/word.hh>

Create a twa_word from a twa_run.

◆ parse_word()

twa_word_ptr spot::parse_word	(	const std::string &	word,
		const bdd_dict_ptr &	dict
	)

#include <spot/twaalgos/word.hh>

Parse a twa_word.

The input should have the form

BF;BF;...;BF;cycle{BF;BF;...;BF}

where BF can be any Boolean formula, and the prefix sequence (before cycle{...}) may be empty.

Parameters

word	the string to parse
dict	the bdd_dict where atomic propositions should be registered

◆ shared_state_deleter()

void spot::shared_state_deleter ( state * s )

inline

#include <spot/twa/twa.hh>

Deleter for shared_state: calls state::destroy().

Use this as the custom deleter when constructing a shared_state from a raw state pointer:

shared_state s(aut->get_init_state(),

spot::shared_state_deleter);

spot::shared_state

std::shared_ptr< const state > shared_state

Shared pointer to a const state.

Definition twa.hh:272

spot::shared_state_deleter

void shared_state_deleter(state *s)

Deleter for shared_state: calls state::destroy().

Definition twa.hh:283

References spot::state::destroy().

Classes

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ bdd_dict_ptr

◆ const_twa_ptr

◆ const_twa_word_ptr

◆ shared_state

◆ twa_ptr

◆ twa_run_ptr

◆ twa_word_ptr

Function Documentation

◆ bdd_format_accset()

◆ bdd_format_formula()

◆ bdd_format_isop()

◆ bdd_format_sat()

◆ bdd_format_set()

◆ bdd_print_accset()

◆ bdd_print_formula()

◆ bdd_print_isop()

◆ bdd_print_sat()

◆ bdd_print_set()

◆ bdd_to_cnf_formula()

◆ bdd_to_formula()

◆ enable_utf8()

◆ formula_to_bdd() [1/2]

◆ formula_to_bdd() [2/2]

◆ make_bdd_dict()

◆ make_twa_word() [1/2]

◆ make_twa_word() [2/2]

◆ parse_word()

◆ shared_state_deleter()