MTBDD-based representation of a state-based ω-automaton. More...

#include <spot/twaalgos/mtdswa.hh>

Inheritance diagram for spot::mtdswa:

Collaboration diagram for spot::mtdswa:

Public Member Functions
	mtdswa (const bdd_dict_ptr &dict) noexcept
	Construct an MTDSwA with the given BDD dictionary. More...

bdd_dict_ptr	get_dict () const
	Get the bdd_dict associated to this automaton. More...

unsigned	num_roots () const
	Return the number of root states. More...

unsigned	num_states () const
	The number of states in the automaton. More...

std::ostream &	print_dot (std::ostream &os, const char *opts=nullptr) const
	Print the MTBDD. More...

twa_graph_ptr	as_twa (bool state_based=false, bool labels=true, bool complete=false) const
	Convert to twa. More...

void	sinks_as_states ()
	Convert bddtrue/bddfalse nodes to actual states. More...

void	sinks_as_constants (bool keep_all_states=false)
	Convert sink states to bddtrue/bddfalse constants. More...

bdd	get_controllable_variables () const
	Returns the conjunction of controllable variables. More...


void	set_controllable_variables (const std::vector< std::string > &vars, bool ignore_non_registered_ap=false)
	Declare a list of controllable variables. More...

void	set_controllable_variables (bdd vars)
	Declare a list of controllable variables. More...

Public Attributes
std::vector< formula >	aps
	The list of atomic propositions possibly used by the automaton. More...

std::vector< bdd >	states
	BDD transitions for each root state. More...

std::vector< formula >	names
	Name formula for each root state. More...

std::vector< acc_cond::mark_t >	colors
	Acceptance marks per root state. More...

acc_cond	acc
	Acceptance condition of the automaton. More...

std::unordered_map< int, int >	terminal_to_state_map
	Map terminal BDD values to state indices (debug only). More...

std::unordered_map< int, unsigned >	highlight_nodes
	Highlighted BDD nodes (for visualization). More...

std::unordered_map< int, int >	highlight_groups
	Cluster grouping for BDD nodes (for visualization). More...

Detailed Description

MTBDD-based representation of a state-based ω-automaton.

Constructor & Destructor Documentation

◆ mtdswa()

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

inlinenoexcept

Construct an MTDSwA with the given BDD dictionary.

Member Function Documentation

◆ as_twa()

twa_graph_ptr spot::mtdswa::as_twa	(	bool	state_based = `false`,
		bool	labels = `true`,
		bool	complete = `false`
	)		const

Convert to twa.

◆ get_controllable_variables()

bdd spot::mtdswa::get_controllable_variables ( ) const

inline

Returns the conjunction of controllable variables.

◆ get_dict()

bdd_dict_ptr spot::mtdswa::get_dict ( ) const

inline

Get the bdd_dict associated to this automaton.

◆ num_roots()

unsigned spot::mtdswa::num_roots ( ) const

inline

Return the number of root states.

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

◆ num_states()

unsigned spot::mtdswa::num_states ( ) const

inline

The number of states in the automaton.

This counts the number of roots, plus one if the bddtrue state is reachable. This is therefore the size that the transition-based output of as_twa() would have.

◆ print_dot()

std::ostream& spot::mtdswa::print_dot	(	std::ostream &	os,
		const char *	opts = `nullptr`
	)		const

Print the MTBDD.

Add opts="s" to show SCCs.

◆ set_controllable_variables() [1/2]

void spot::mtdswa::set_controllable_variables ( bdd vars )

Declare a list of controllable variables.

Doing so affects the way the automaton is printed in dot format, but this is also a prerequisite for interpreting the automaton as a game.

This function is expected to be called after you have built the automaton, in some way (causing atomic propositions to be registered). If ignore_non_registered_ap is set, variable listed as output but not registered by the automaton will be dropped. Else, an exception will be raised for those variables.

◆ set_controllable_variables() [2/2]

void spot::mtdswa::set_controllable_variables	(	const std::vector< std::string > &	vars,
		bool	ignore_non_registered_ap = `false`
	)

Declare a list of controllable variables.

Doing so affects the way the automaton is printed in dot format, but this is also a prerequisite for interpreting the automaton as a game.

This function is expected to be called after you have built the automaton, in some way (causing atomic propositions to be registered). If ignore_non_registered_ap is set, variable listed as output but not registered by the automaton will be dropped. Else, an exception will be raised for those variables.

◆ sinks_as_constants()

void spot::mtdswa::sinks_as_constants ( bool keep_all_states = false )

Convert sink states to bddtrue/bddfalse constants.

This modifies the automaton in place so that any sink state is turned into bddtrue or bddfalse depending on its acceptance.

The original sink states will be removed and the other state will be renumbered, unless keep_all_states is set.

◆ sinks_as_states()

void spot::mtdswa::sinks_as_states ( )

Convert bddtrue/bddfalse nodes to actual states.

This modifies the automaton in place so that it does not use the bddtrue and bddfalse constants. Those will be replaced by accepting and rejecting sinks respectively. Those new states are introduced only if no existing state can serve the same purpose.

When the acceptance condition is always accepting, or when it is always rejecting, introducing a sink state might require changing the acceptance condition. When that happens, the acceptance will be set to Büchi.

If the automaton had named states, newly introduced sinks will be named as formula::tt() or formula::ff().

Member Data Documentation

◆ acc

acc_cond spot::mtdswa::acc

Acceptance condition of the automaton.

◆ aps

std::vector<formula> spot::mtdswa::aps

The list of atomic propositions possibly used by the automaton.

This is actually the list of atomic propositions that appeared in the formulas/automata that were used to build this automaton. The automaton itself may use fewer atomic propositions, for instance in case some of them cancel each other.

This vector is sorted by formula ID, to make it easy to merge with another sorted vector.

◆ colors

std::vector<acc_cond::mark_t> spot::mtdswa::colors

Acceptance marks per root state.

◆ highlight_groups

std::unordered_map<int, int> spot::mtdswa::highlight_groups

Cluster grouping for BDD nodes (for visualization).

◆ highlight_nodes

std::unordered_map<int, unsigned> spot::mtdswa::highlight_nodes

Highlighted BDD nodes (for visualization).

◆ names

std::vector<formula> spot::mtdswa::names

Name formula for each root state.

◆ states

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

BDD transitions for each root state.

◆ terminal_to_state_map

std::unordered_map<int, int> spot::mtdswa::terminal_to_state_map

Map terminal BDD values to state indices (debug only).

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

spot/twaalgos/mtdswa.hh

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ mtdswa()

Member Function Documentation

◆ as_twa()

◆ get_controllable_variables()

◆ get_dict()

◆ num_roots()

◆ num_states()

◆ print_dot()

◆ set_controllable_variables() [1/2]

◆ set_controllable_variables() [2/2]

◆ sinks_as_constants()

◆ sinks_as_states()

Member Data Documentation

◆ acc

◆ aps

◆ colors

◆ highlight_groups

◆ highlight_nodes

◆ names

◆ states

◆ terminal_to_state_map