TωA cube algorithms

Functions
spot::cube	spot::satone_to_cube (bdd one, cubeset &cubeset, std::unordered_map< int, int > &binder)
	Transform one truth assignment represented as a BDD into a cube cube passed in parameter. The parameter binder map bdd indexes to cube indexes.
bdd	spot::cube_to_bdd (spot::cube cube, const cubeset &cubeset, std::unordered_map< int, int > &reverse_binder)
	Transform a cube cube into a BDD using the map that binds cube indexes to BDD indexes.
std::vector< std::string > *	spot::extract_aps (spot::const_twa_graph_ptr aut, std::unordered_map< int, int > &ap_binder)
	Extract the atomic propositions from the automaton. This method also fills the binder, i.e., the mapping between BDD indexes and cube indexes.
twacube_ptr	spot::twa_to_twacube (spot::const_twa_graph_ptr aut)
	Convert a twa into a twacube.
spot::twa_graph_ptr	spot::twacube_to_twa (spot::twacube_ptr twacube, spot::bdd_dict_ptr d=nullptr)
	Convert a twacube into a twa. When d is specified, the BDD_dict in parameter is used rather than creating a new one.
bool	spot::are_equivalent (const spot::twacube_ptr twacube, const spot::const_twa_graph_ptr twa)
	Check whether a twacube and a twa are equivalent.

Detailed Description

Function Documentation

are_equivalent()

bool spot::are_equivalent	(	const spot::twacube_ptr	twacube,
		const spot::const_twa_graph_ptr	twa
	)

#include <spot/twacube_algos/convert.hh>

Check whether a twacube and a twa are equivalent.

cube_to_bdd()

bdd spot::cube_to_bdd	(	spot::cube	cube,
		const cubeset &	cubeset,
		std::unordered_map< int, int > &	reverse_binder
	)

#include <spot/twacube_algos/convert.hh>

Transform a cube cube into a BDD using the map that binds cube indexes to BDD indexes.

Referenced by spot::kripkecube_to_twa< State, SuccIterator, StateHash, StateEqual >::edge(), spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::push_state(), and spot::product_to_twa< State, SuccIterator, StateHash, StateEqual >::update().

extract_aps()

std::vector< std::string > * spot::extract_aps	(	spot::const_twa_graph_ptr	aut,
		std::unordered_map< int, int > &	ap_binder
	)

#include <spot/twacube_algos/convert.hh>

Extract the atomic propositions from the automaton. This method also fills the binder, i.e., the mapping between BDD indexes and cube indexes.

satone_to_cube()

spot::cube spot::satone_to_cube	(	bdd	one,
		cubeset &	cubeset,
		std::unordered_map< int, int > &	binder
	)

#include <spot/twacube_algos/convert.hh>

Transform one truth assignment represented as a BDD into a cube cube passed in parameter. The parameter binder map bdd indexes to cube indexes.

twa_to_twacube()

twacube_ptr spot::twa_to_twacube

(

spot::const_twa_graph_ptr

aut

)

#include <spot/twacube_algos/convert.hh>

Convert a twa into a twacube.

twacube_to_twa()

spot::twa_graph_ptr spot::twacube_to_twa	(	spot::twacube_ptr	twacube,
		spot::bdd_dict_ptr	d = nullptr
	)

#include <spot/twacube_algos/convert.hh>

Convert a twacube into a twa. When d is specified, the BDD_dict in parameter is used rather than creating a new one.