spot::mtdtwa Struct Reference

A multi-terminal decision diagram representation of a TωA. More...

#include <spot/twaalgos/mtdtwa.hh>

Inheritance diagram for spot::mtdtwa:

Collaboration diagram for spot::mtdtwa:

Public Member Functions
	mtdtwa (const bdd_dict_ptr &dict) noexcept
	Construct an MTDTwA with the given BDD dictionary.
unsigned	num_roots () const
	Return the number of root states.
std::ostream &	print_dot (std::ostream &os) const
	Print the MTBDD in dot format.
twa_graph_ptr	as_twa (bool state_based=false, bool labels=true) const
	Convert to a twa_graph.

Public Attributes
std::vector< bdd >	states
	BDD transitions for each root state.
acc_cond	acc
	Acceptance condition of the automaton.
bdd_dict_ptr	dict_
terminal_data_map_t	terminal_data_map
	Map from terminal BDD values to data.

Detailed Description

A multi-terminal decision diagram representation of a TωA.

Constructor & Destructor Documentation

mtdtwa()

spot::mtdtwa::mtdtwa ( const bdd_dict_ptr &  dict )

inlinenoexcept

Construct an MTDTwA with the given BDD dictionary.

Member Function Documentation

as_twa()

twa_graph_ptr spot::mtdtwa::as_twa	(	bool	state_based = false,
		bool	labels = true
	)		const

Convert to a twa_graph.

num_roots()

unsigned spot::mtdtwa::num_roots ( ) const

inline

Return the number of root states.

Note that this does not include bddtrue and bddfalse even if they are reachable.

print_dot()

std::ostream & spot::mtdtwa::print_dot

(

std::ostream &

os

)

const

Print the MTBDD in dot format.

Member Data Documentation

acc

acc_cond spot::mtdtwa::acc

Acceptance condition of the automaton.

dict_

bdd_dict_ptr spot::mtdtwa::dict_

BDD dictionary.

states

std::vector<bdd> spot::mtdtwa::states

BDD transitions for each root state.

terminal_data_map

terminal_data_map_t spot::mtdtwa::terminal_data_map

Map from terminal BDD values to data.

---

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

• spot/twaalgos/mtdtwa.hh